proposition: Lemma card_vspace (V : {vspace vT}) : #|V| = (#|F| ^ \dim V)%N.
proof: Proof. set n := \dim V; pose V2rV v := \row_i coord (vbasis V) i v. pose rV2V (rv : 'rV_n) := \sum_i rv 0 i *: (vbasis V)`_i. have rV2V_K: cancel rV2V V2rV. have freeV: free (vbasis V) := basis_free (vbasisP V). by move=> rv; apply/rowP=> i; rewrite mxE coord_sum_free. rewrite -[n]mul1n -card_mx -(card_imset _ (can_inj rV2V_K)). apply: eq_card => v; apply/idP/imsetP=> [/coord_vbasis-> | [rv _ ->]]. by exists (V2rV v) => //; apply: eq_bigr => i _; rewrite mxE. by apply: (@rpred_sum vT) => i _; rewrite rpredZ ?vbasis_mem ?memt_nth. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype div tuple bigop prime finset fingroup) mathcomp(ssralg poly polydiv morphism action countalg) mathcomp(finalg zmodp cyclic center pgroup abelian matrix) mathcomp(mxpoly vector falgebra fieldext separable galois)