mathlib3

d5c6f614 - feat(algebra/group/hom): monoid_hom.injective_iff in iff form (#8259)

feat(algebra/group/hom): monoid_hom.injective_iff in iff form (#8259) Interpret the injectivity of a group hom as triviality of the kernel, in iff form. This helps make explicit simp lemmas about the application of such homs, as in the added `extend_domain_eq_one_iff` lemma. Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>