proposition: Lemma submod_mx_irr : mx_irreducible rU <-> mxsimple rG U.
proof: Proof. split=> [] [_ nzU simU]. rewrite -mxrank_eq0 mxrank1 mxrank_eq0 in nzU; split=> // V modV sVU nzV. rewrite -(in_submodK sVU) -val_submod1 val_submodS. rewrite -(genmxE (in_submod U V)) simU ?genmxE ?submx1 //=. by rewrite (eqmx_module _ (genmxE _)) in_submod_module. rewrite -submx0 genmxE -val_submodS in_submodK //. by rewrite linear0 eqmx0 submx0. apply/mx_irrP; rewrite lt0n mxrank_eq0; split=> // V modV. rewrite -(inj_eq val_submod_inj) linear0 -(eqmx_eq0 (genmxE _)) => nzV. rewrite -sub1mx -val_submodS val_submod1 -(genmxE (val_submod V)). rewrite simU ?genmxE ?val_submodP //=. by rewrite (eqmx_module _ (genmxE _)) val_submod_module. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)