proposition: Lemma rfix_regular : (rfix_mx aG G :=: gring_row (gset_mx G))%MS.
proof: Proof. apply/eqmxP/andP; split; last first. apply/rfix_mxP => x Gx; rewrite -gring_row_mul; congr gring_row. rewrite {2}/gset_mx (reindex_astabs 'R x) ?astabsR //= mulmx_suml. by apply: eq_bigr => y Gy; rewrite repr_mxM. apply/rV_subP=> v /rfix_mxP cGv. have /envelop_mxP[a def_v]: (gring_mx aG v \in R_G)%MS. by rewrite vec_mxK submxMl. suffices ->: v = a 1%g *: gring_row (gset_mx G) by rewrite scalemx_sub. rewrite -linearZ scaler_sumr -[v]gring_mxK def_v; congr (gring_row _). apply: eq_bigr => x Gx; congr (_ *: _). move/rowP/(_ 0): (congr1 (gring_proj x \o gring_mx aG) (cGv x Gx)). rewrite /= gring_mxJ // def_v mulmx_suml !linear_sum (bigD1 1%g) //=. rewrite repr_mx1 -scalemxAl mul1mx linearZ /= gring_projE // eqxx scalemx1. rewrite big1 ?addr0 ?mxE /= => [ | y /andP[Gy nt_y]]; last first. rewrite -scalemxAl linearZ -repr_mxM //= gring_projE ?groupM //. by rewrite eq_sym eq_mulgV1 mulgK (negPf nt_y) scaler0. rewrite (bigD1 x) //= linearZ /= gring_projE // eqxx scalemx1. rewrite big1 ?addr0 ?mxE // => y /andP[Gy ne_yx]. by rewrite linearZ /= gring_projE // eq_sym (negPf ne_yx) scaler0. 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)