proposition: Lemma ahomP {f : 'Hom(aT, rT)} : reflect (multiplicative f) (ahom_in {:aT} f).
proof: Proof. apply: (iffP ahom_inP) => [[fM f1] | fRM_P]; last first. by split=> [x y|]; [rewrite fRM_P.1|rewrite fRM_P.2]. by split=> // x y; rewrite fM ?memvf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop ssralg) mathcomp(finalg zmodp matrix vector poly)