proposition: Fact matrix_vect_iso : Vector.axiom (m * n) 'M[R]_(m, n).
proof: Proof. exists mxvec => /=; first exact: linearP. by exists vec_mx; [apply: mxvecK | apply: vec_mxK]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)