proposition: Fact lfun_vect_iso : Vector.axiom (dim aT * dim rT) 'Hom(aT, rT).
proof: Proof. exists (mxvec \o f2mx) => [a f g|]. rewrite /= -linearP /= -[A in _ = mxvec A]/(f2mx (Hom _)). congr (mxvec (f2mx _)); apply/lfunP=> v; do 2!rewrite lfunE /=. by rewrite unlock /= -linearP mulmxDr scalemxAr. apply: Bijective (Hom \o vec_mx) _ _ => [[A]|A] /=; last exact: vec_mxK. by rewrite mxvecK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)