proposition: Lemma ker_factm_loc (K : {group aT}) : 'ker_(q @* K) ff = q @* 'ker_K f.
proof: Proof. by rewrite ker_factm -morphimIG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)