Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-30 17:18 c10efa66

View on Github →

refactor(algebra/hom/group): generalize basic API of monoid_hom to monoid_hom_class (#14997) This PR generalizes part of the basic API of monoid homs to monoid_hom_class. This notably includes things like monoid_hom.mker, submonoid.map and submonoid.comap. I left the namespaces unchanged, for example monoid_hom.mker remains the same even though it is now defined for any monoid_hom_class morphism; this way dot notation still (mostly) works for actual monoid homs.

Estimated changes

modified theorem submonoid.map_powers
modified theorem monoid_hom.coe_mker
modified theorem monoid_hom.coe_mrange
modified theorem monoid_hom.comap_bot'
modified theorem monoid_hom.map_mclosure
modified theorem monoid_hom.mem_mker
modified theorem monoid_hom.mem_mrange
modified def monoid_hom.mker
modified def monoid_hom.mrange
modified theorem monoid_hom.mrange_eq_map
modified theorem submonoid.apply_coe_mem_map
modified theorem submonoid.coe_comap
modified theorem submonoid.coe_map
modified def submonoid.comap
modified theorem submonoid.comap_id
modified theorem submonoid.comap_inf
modified theorem submonoid.comap_infi
modified theorem submonoid.comap_map_comap
modified theorem submonoid.comap_top
modified theorem submonoid.gc_map_comap
modified theorem submonoid.le_comap_map
modified def submonoid.map
modified theorem submonoid.map_bot
modified theorem submonoid.map_comap_le
modified theorem submonoid.map_comap_map
modified theorem submonoid.map_sup
modified theorem submonoid.map_supr
modified theorem submonoid.mem_comap
modified theorem submonoid.mem_map
modified theorem submonoid.mem_map_iff_mem
modified theorem submonoid.mem_map_of_mem
modified theorem submonoid.monotone_comap
modified theorem submonoid.monotone_map