proposition: Lemma dim_vspaceOver M : (F * M <= M)%VS -> \dim (vspaceOver M) = \dim_F M.
proof: Proof. move=> modM; have [] := field_module_semisimple modM. set n := \dim_F M => b [Mb nz_b] [defM dx_b]. suff: basis_of (vspaceOver M) b by apply: size_basis. apply/andP; split. rewrite eqEsubv; apply/andP; split; apply/span_subvP=> u. by rewrite mem_vspaceOver field_module_eq // => /Mb. move/(@vbasis_mem _ _ _ M); rewrite -defM => /memv_sumP[{}u Fu ->]. apply: memv_suml => i _; have /memv_cosetP[a Fa ->] := Fu i isT. by apply: (memvZ (Subvs Fa)); rewrite memv_span ?memt_nth. apply/freeP=> a /(directv_sum_independent dx_b) a_0 i. have{a_0}: a i *: (b`_i : L_F) == 0. by rewrite a_0 {i}// => i _; rewrite memv_mul ?memv_line ?subvsP. by rewrite scaler_eq0=> /predU1P[] // /idPn[]; rewrite (memPn nz_b) ?memt_nth. 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)