proposition: Lemma mx_abs_irr_cent_scalar : mx_absolutely_irreducible -> forall A, centgmx rG A -> is_scalar_mx A.
proof: Proof. case/mx_abs_irrP=> n_gt0 [a_ a_G] A /centgmxP cGA. have{cGA a_G} cMA B: A *m B = B *m A. rewrite {}[B]a_G mulmx_suml mulmx_sumr. by apply: eq_bigr => x Gx; rewrite -scalemxAl -scalemxAr cGA. pose i0 := Ordinal n_gt0; apply/is_scalar_mxP; exists (A i0 i0). apply/matrixP=> i j; move/matrixP/(_ i0 j): (esym (cMA (delta_mx i0 i))). rewrite -[A *m _]trmxK trmx_mul trmx_delta -!(@mul_delta_mx _ n 1 n 0) -!mulmxA. by rewrite -!rowE !mxE !big_ord1 !mxE !eqxx !mulr_natl /= andbT eq_sym. 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)