Commit 2021-07-12 01:47 d5c6f614
View on Github →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.