proposition: Lemma morphpre_mx_abs_irr : G \subset f @* D -> mx_absolutely_irreducible rGf = mx_absolutely_irreducible rG.
proof: Proof. move=> sGfD; congr (_ && (_ == _)); apply/eqP; rewrite mxrank_leqif_sup //. apply/row_subP=> i; rewrite rowK. case/morphimP: (subsetP sGfD _ (enum_valP i)) => x Dx _ def_i. by rewrite def_i (envelop_mx_id rGf) // !inE Dx -def_i enum_valP. apply/row_subP=> i; rewrite rowK (envelop_mx_id rG) //. by case/morphpreP: (enum_valP i). 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)