proposition: Lemma regular_mx_faithful : mx_faithful aG.
proof: Proof. apply/subsetP=> x /setIdP[Gx]. rewrite mul1mx inE => /eqP/(congr1 (gring_proj 1%g)). rewrite -(repr_mx1 aG) !gring_projE ?group1 // eqxx eq_sym. by case: (x == _) => // /eqP; rewrite eq_sym oner_eq0. 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)