proposition: Fact baseField_vectMixin : Lmodule_hasFinDim F0 L0.
proof: Proof. pose bL := vbasis {:L}; set m := \dim {:L} in bL. pose v2r (x : L0) := mxvec (\matrix_(i, j) coord bF j (coord bL i x)). have v2r_lin: linear v2r. move=> a x y; rewrite -linearP; congr (mxvec _); apply/matrixP=> i j. by rewrite !mxE linearP /= mulr_algl linearP. pose r2v r := \sum_(i < m) (\sum_(j < n) vec_mx r i j *: bF`_j) *: bL`_i. have v2rK: cancel v2r r2v. move=> x; transitivity (\sum_(i < m) coord bL i x *: bL`_i); last first. by rewrite -coord_vbasis ?memvf. apply: eq_bigr => i _; rewrite mxvecK; congr (_ *: _ : L). by rewrite (coordF (coord bL i x)); apply: eq_bigr => j _; rewrite mxE. exists (m * n)%N, v2r => //; exists r2v => // r. apply: (canLR vec_mxK); apply/matrixP=> i j; rewrite mxE. by rewrite !coord_sum_free ?(basis_free (vbasisP _)). 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)