proposition: Lemma dim_baseVspace V : \dim (baseVspace V) = (\dim V * n)%N.
proof: Proof. pose bV0 := baseVspace_basis V; set m := \dim V in bV0 *. suffices /size_basis->: basis_of (baseVspace V) bV0. by rewrite card_prod !card_ord. rewrite /basis_of eqxx. apply/freeP=> s sb0 k; rewrite -(enum_valK k); case/enum_val: k => i j. have free_baseP := freeP (basis_free (vbasisP _)). move: j; apply: (free_baseP _ _ fullv); move: i; apply: (free_baseP _ _ V). transitivity (\sum_i \sum_j s (enum_rank (i, j)) *: bV0`_(enum_rank (i, j))). apply: eq_bigr => i _; rewrite scaler_suml; apply: eq_bigr => j _. by rewrite -F0ZEZ nth_image enum_rankK -!tnth_nth. rewrite pair_bigA (reindex _ (onW_bij _ (enum_val_bij _))); apply: etrans sb0. by apply: eq_bigr => k _; rewrite -{5 6}[k](enum_valK k); case/enum_val: k. 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)