proposition: Fact fieldOver_vectMixin : Lmodule_hasFinDim K_F L_F.
proof: Proof. have [bL [_ nz_bL] [defL dxSbL]] := field_module_semisimple (subvf (F * _)). do [set n := \dim_F {:L} in bL nz_bL *; set SbL := (\sum_i _)%VS] in defL dxSbL. have in_bL i (a : K_F) : val a * (bL`_i : L_F) \in (F * <[bL`_i]>)%VS. by rewrite memv_mul ?(valP a) ?memv_line. have nz_bLi (i : 'I_n): bL`_i != 0 by rewrite (memPn nz_bL) ?memt_nth. pose r2v (v : 'rV[K_F]_n) : L_F := \sum_i v 0 i *: (bL`_i : L_F). have r2v_lin: linear r2v. move=> a u v; rewrite /r2v scaler_sumr -big_split /=; apply: eq_bigr => i _. by rewrite scalerA -scalerDl !mxE. pose r2vlM := GRing.isLinear.Build _ _ _ _ r2v r2v_lin. pose r2vL : GRing.Linear.type _ _ := HB.pack r2v r2vlM. have v2rP x: {r : 'rV[K_F]_n | x = r2v r}. apply: sig_eqW; have /memv_sumP[y Fy ->]: x \in SbL by rewrite defL memvf. have /fin_all_exists[r Dr] i: exists r, y i = r *: (bL`_i : L_F). by have /memv_cosetP[a Fa ->] := Fy i isT; exists (Subvs Fa). by exists (\row_i r i); apply: eq_bigr => i _; rewrite mxE. pose v2r x := sval (v2rP x). have v2rK: cancel v2r r2vL by rewrite /v2r => x; case: (v2rP x). suffices r2vK: cancel r2v v2r. by exists n, v2r; [apply: can2_linear v2rK | exists r2v]. move=> r; apply/rowP=> i; apply/val_inj/(mulIf (nz_bLi i))/eqP; move: i isT. by apply/forall_inP; move/directv_sum_unique: dxSbL => <- //; apply/eqP/v2rK. 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)