proposition: Lemma rker_gen : rker rGA = rker rG.
proof: Proof. apply/setP=> g; rewrite !inE !mul1mx; case Gg: (g \in G) => //=. apply/eqP/eqP=> g1; apply/row_matrixP=> i. by apply: (can_inj in_genK); rewrite rowE in_genJ //= g1 mulmx1 row1. by apply: (can_inj val_genK); rewrite rowE val_genJ //= g1 mulmx1 row1. 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)