fact: Definition ahom_in (U : {vspace aT}) (f : 'Hom(aT, rT)) := all2rel (fun x y : aT => f (x * y) == f x * f y) (vbasis U) && (f 1 == 1).
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)