proposition: Lemma kerP x : x \in D -> reflect (f x = 1) (x \in 'ker f).
proof: Proof. by move=> Dx; rewrite 2!inE Dx; apply: set1P. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)