proposition: Lemma limg_basis_of f U X : (U :&: lker f = 0)%VS -> basis_of U X -> basis_of (f @: U) (map f X).
proof: Proof. move=> injUf /andP[/eqP defU /eqnP freeX]. by rewrite /basis_of /free size_map -limg_span -freeX defU limg_dim_eq ?eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)