proposition: Lemma kHom_dim K E f : kHom K E f -> \dim (f @: E) = \dim E.
proof: Proof. move=> homKf; have [fM idKf] := kHomP homKf. apply/limg_dim_eq/eqP; rewrite -subv0; apply/subvP=> v. rewrite memv_cap memv0 memv_ker => /andP[Ev]; apply: contraLR => nz_v. by rewrite -unitfE unitrE -(kHom_inv homKf) // -fM ?rpredV ?divff ?idKf ?mem1v. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)