proposition: Lemma non_linear_gen_reducible : d > 1 -> mxnonsimple (map_repr gen rG) 1%:M.
proof: Proof. rewrite ltnNge mxminpoly_linear_is_scalar => Anscal. pose Af := map_mx gen A; exists (kermx (Af - groot%:M)). rewrite submx1 kermx_centg_module /=; last first. apply/centgmxP=> z Gz; rewrite mulmxBl mulmxBr scalar_mxC. by rewrite -!map_mxM 1?(centgmxP cGA). rewrite andbC mxrank_ker -subn_gt0 mxrank1 subKn ?rank_leq_row // lt0n. rewrite mxrank_eq0 subr_eq0; case: eqP => [defAf | _]. rewrite -(map_mx_is_scalar gen) -/Af in Anscal. by case/is_scalar_mxP: Anscal; exists groot. rewrite -mxrank_eq0 mxrank_ker subn_eq0 row_leq_rank. apply/row_freeP=> [[XA' XAK]]. have pAf0: (mxminpoly Af).[groot] == 0. by rewrite mxminpoly_map ?map_mxminpoly_groot. have{pAf0} [q def_pAf]:= factor_theorem _ _ pAf0. have q_nz: q != 0. case: eqP (congr1 (fun p : {poly _} => size p) def_pAf) => // ->. by rewrite size_mxminpoly mul0r size_poly0. have qAf0: horner_mx Af q = 0. rewrite -[_ q]mulr1 -[1]XAK mulrA -{2}(horner_mx_X Af) -(horner_mx_C Af). by rewrite -rmorphB -rmorphM -def_pAf /= mx_root_minpoly mul0r. have{qAf0} := dvdp_leq q_nz (mxminpoly_min qAf0); rewrite def_pAf. by rewrite size_Mmonic ?monicXsubC // polyseqXsubC addn2 ltnn. 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)