proposition: Lemma mkerr x y : x \in D -> y \in 'ker f -> f (x * y) = f x.
proof: Proof. by move=> Dx Ky; rewrite morphM // ?(dom_ker, mker Ky, mulg1). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)