proposition: Lemma field_module_semisimple F M (m := \dim_F M) : (F * M <= M)%VS -> {X : m.-tuple L | {subset X <= M} /\ 0 \notin X & let FX := (\sum_(i < m) F * <[X`_i]>)%VS in FX = M /\ directv FX}.
proof: Proof. move=> modM; have dimM: (m * \dim F)%N = \dim M by rewrite -dim_field_module. have [X [defM dxFX nzX]] := skew_field_module_semisimple (@fieldP L) modM. have szX: size X == m. rewrite -(eqn_pmul2r (adim_gt0 F)) dimM -defM (directvP dxFX) /=. rewrite -sum1_size big_distrl; apply/eqP/eq_big_seq => x Xx /=. by rewrite mul1n dim_cosetv ?(memPn nzX). rewrite directvE /= (big_nth 0) [eqbRHS](big_nth 0) in defM dxFX. rewrite (eqP szX) !big_mkord -directvE in defM dxFX. exists (Tuple szX) => //; split=> // _ /tnthP[i ->]; rewrite (tnth_nth 0) /=. by rewrite -defM memvE (sumv_sup i) ?field_subvMl. 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)