proposition: Lemma mx_group_homocyclic m n q : homocyclic [set: 'M['Z_q]_(m, n)].
proof: Proof. wlog q_gt1: q / q > 1 by case: q => [|[|q -> //]] /(_ 2)->. set G := setT; have cGG: abelian G := zmod_abelian _. rewrite -max_card_abelian //= rank_mx_group cardsT card_mx card_ord -/G. rewrite {1}Zp_cast //; have [-> // | ] := posnP (m * n). by rewrite muln_gt0 => /andP[m_gt0 n_gt0]; rewrite exponent_mx_group. 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)