proposition: Fact aimg_is_aspace (rT : falgType F0) (f : 'AHom(L, rT)) (E : {subfield L}) : is_aspace (f @: E).
proof: Proof. rewrite /is_aspace -aimgM limgS ?prodv_id // has_algid1 //. by apply/memv_imgP; exists 1; rewrite ?mem1v ?rmorph1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)