proposition: Lemma rank_mx_group m n q : 'r([set: 'M['Z_q]_(m, n)]) = (m * n)%N.
proof: Proof. wlog q_gt1: q / q > 1 by case: q => [|[|q -> //]] /(_ 2)->. set G := setT; have cGG: abelian G := zmod_abelian _. have [mn0 | ] := posnP (m * n). by rewrite [G](card1_trivg _) ?rank1 // cardsT card_mx mn0. rewrite muln_gt0 => /andP[m_gt0 n_gt0]. have expG: exponent G = q := exponent_mx_group m_gt0 n_gt0 q_gt1. apply/eqP; rewrite eqn_leq andbC -(leq_exp2l _ _ q_gt1) -{2}expG. have ->: (q ^ (m * n))%N = #|G| by rewrite cardsT card_mx card_ord Zp_cast. rewrite max_card_abelian //= -grank_abelian //= -/G. pose B : {set 'M['Z_q]_(m, n)} := [set delta_mx ij.1 ij.2 | ij : 'I_m * 'I_n]. suffices ->: G = <<B>>. have ->: (m * n)%N = #|{: 'I_m * 'I_n}| by rewrite card_prod !card_ord. exact: leq_trans (grank_min _) (leq_imset_card _ _). apply/setP=> v; rewrite inE (matrix_sum_delta v). rewrite group_prod // => i _; rewrite group_prod // => j _. rewrite -[v i j]natr_Zp scaler_nat groupX // mem_gen //. by apply/imsetP; exists (i, j). 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)