Commit 2022-11-29 12:34 4f81077a

View on Github →

feat(group_theory/subgroup/basic): generalize monoid_hom.eq_locus (#17748) Only assume that the codomain is a monoid. Also rename monoid_hom.gclosure_preimage_le to monoid_hom.closure_preimage_le.

Estimated changes

Modified src/group_theory/subgroup/basic.lean

added theorem monoid_hom.closure_preimage_le

modified def monoid_hom.eq_locus

modified theorem monoid_hom.eq_of_eq_on_dense

modified theorem monoid_hom.eq_of_eq_on_top

modified theorem monoid_hom.eq_on_closure

deleted theorem monoid_hom.gclosure_preimage_le