Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-26 18:41 76de6f75

View on Github →

feat(group_theory/subsemigroup/operations): port from submonoid (#12112) Taken from group_theory.submonoid.operations, trying to keep as much API as possible

Estimated changes

added theorem mul_hom.coe_srange
added theorem mul_hom.map_mclosure
added theorem mul_hom.map_srange
added theorem mul_hom.mem_srange
added def mul_hom.srange
added theorem mul_hom.srange_eq_map
added theorem mul_mem_class.coe_mul
added theorem mul_mem_class.mul_def
added theorem subsemigroup.coe_comap
added theorem subsemigroup.coe_map
added theorem subsemigroup.coe_prod
added theorem subsemigroup.comap_id
added theorem subsemigroup.comap_inf
added theorem subsemigroup.comap_top
added def subsemigroup.map
added theorem subsemigroup.map_bot
added theorem subsemigroup.map_id
added theorem subsemigroup.map_map
added theorem subsemigroup.map_sup
added theorem subsemigroup.map_supr
added theorem subsemigroup.mem_comap
added theorem subsemigroup.mem_map
added theorem subsemigroup.mem_prod
added theorem subsemigroup.prod_mono
added theorem subsemigroup.prod_top
added theorem subsemigroup.top_prod