proposition: Lemma exponent_mx_group m n q : m > 0 -> n > 0 -> q > 1 -> exponent [set: 'M['Z_q]_(m, n)] = q.
proof: Proof. move=> m_gt0 n_gt0 q_gt1; apply/eqP; rewrite eqn_dvd; apply/andP; split. apply/exponentP=> x _; apply/matrixP=> i j; rewrite mulmxnE !mxE. by rewrite -mulr_natr -Zp_nat_mod // modnn mulr0. pose cmx1 := const_mx 1%R : 'M['Z_q]_(m, n). apply: dvdn_trans (dvdn_exponent (in_setT cmx1)). have/matrixP/(_ (Ordinal m_gt0))/(_ (Ordinal n_gt0))/eqP := expg_order cmx1. by rewrite mulmxnE !mxE -order_dvdn order_Zp1 Zp_cast. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient gproduct action finalg) mathcomp(zmodp commutator cyclic center pgroup gseries) mathcomp(nilpotent sylow maximal abelian matrix) mathcomp(mxalgebra mxrepresentation)