proposition: Lemma mx_abs_irrW : mx_absolutely_irreducible -> mx_irreducible.
proof: Proof. case/mx_abs_irrP=> n_gt0 [a_ a_G]; apply/mx_irrP; split=> // U Umod. case/rowV0Pn=> u Uu; rewrite -mxrank_eq0 -lt0n row_leq_rank -sub1mx. case/submxP: Uu => v ->{u} /row_freeP[u' vK]; apply/row_subP=> i. rewrite rowE scalar_mxC -{}vK -2![_ *m _]mulmxA; move: {u' i}(u' *m _) => A. rewrite mulmx_sub {v}// [A]a_G linear_sum summx_sub //= => x Gx. by rewrite linearZ /= scalemx_sub // (mxmoduleP Umod). 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)