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

Modified src/field_theory/intermediate_field.lean

Modified src/group_theory/submonoid/operations.lean

deleted theorem submonoid_class.coe_mul

deleted theorem submonoid_class.mk_mul_mk

deleted theorem submonoid_class.mul_def

Created src/group_theory/subsemigroup/operations.lean

added def add_subsemigroup.to_subsemigroup'

added theorem add_subsemigroup.to_subsemigroup'_closure

added def add_subsemigroup.to_subsemigroup

added theorem add_subsemigroup.to_subsemigroup_closure

added def mul_equiv.of_left_inverse

added def mul_equiv.subsemigroup_congr

added def mul_equiv.subsemigroup_map

added def mul_hom.cod_srestrict

added theorem mul_hom.coe_srange

added theorem mul_hom.coe_srange_restrict

added theorem mul_hom.map_mclosure

added theorem mul_hom.map_srange

added theorem mul_hom.mclosure_preimage_le

added theorem mul_hom.mem_srange

added theorem mul_hom.prod_map_comap_prod'

added def mul_hom.srange

added theorem mul_hom.srange_eq_map

added def mul_hom.srange_restrict

added theorem mul_hom.srange_restrict_surjective

added theorem mul_hom.srange_top_iff_surjective

added theorem mul_hom.srange_top_of_surjective

added def mul_hom.srestrict

added theorem mul_hom.srestrict_apply

added def mul_hom.subsemigroup_comap

added def mul_hom.subsemigroup_map

added theorem mul_hom.subsemigroup_map_surjective

added theorem mul_mem_class.coe_mul

added theorem mul_mem_class.coe_subtype

added theorem mul_mem_class.mk_mul_mk

added theorem mul_mem_class.mul_def

added def mul_mem_class.subtype

added theorem subsemigroup.apply_coe_mem_map

added theorem subsemigroup.bot_prod_bot

added theorem subsemigroup.closure_closure_coe_preimage

added theorem subsemigroup.coe_comap

added theorem subsemigroup.coe_equiv_map_of_injective_apply

added theorem subsemigroup.coe_map

added theorem subsemigroup.coe_prod

added def subsemigroup.comap

added theorem subsemigroup.comap_comap

added theorem subsemigroup.comap_equiv_eq_map_symm

added theorem subsemigroup.comap_id

added theorem subsemigroup.comap_inf

added theorem subsemigroup.comap_inf_map_of_injective

added theorem subsemigroup.comap_infi

added theorem subsemigroup.comap_infi_map_of_injective

added theorem subsemigroup.comap_injective_of_surjective

added theorem subsemigroup.comap_le_comap_iff_of_surjective

added theorem subsemigroup.comap_map_comap

added theorem subsemigroup.comap_map_eq_of_injective

added theorem subsemigroup.comap_strict_mono_of_surjective

added theorem subsemigroup.comap_sup_map_of_injective

added theorem subsemigroup.comap_supr_map_of_injective

added theorem subsemigroup.comap_surjective_of_injective

added theorem subsemigroup.comap_top

added theorem subsemigroup.eq_top_iff'

added theorem subsemigroup.gc_map_comap

added def subsemigroup.gci_map_comap

added def subsemigroup.gi_map_comap

added def subsemigroup.inclusion

added theorem subsemigroup.le_comap_map

added theorem subsemigroup.le_comap_of_map_le

added theorem subsemigroup.le_prod_iff

added def subsemigroup.map

added theorem subsemigroup.map_bot

added theorem subsemigroup.map_comap_eq_of_surjective

added theorem subsemigroup.map_comap_le

added theorem subsemigroup.map_comap_map

added theorem subsemigroup.map_equiv_eq_comap_symm

added theorem subsemigroup.map_equiv_top

added theorem subsemigroup.map_id

added theorem subsemigroup.map_inf_comap_of_surjective

added theorem subsemigroup.map_infi_comap_of_surjective

added theorem subsemigroup.map_injective_of_injective

added theorem subsemigroup.map_le_iff_le_comap

added theorem subsemigroup.map_le_map_iff_of_injective

added theorem subsemigroup.map_le_of_le_comap

added theorem subsemigroup.map_map

added theorem subsemigroup.map_strict_mono_of_injective

added theorem subsemigroup.map_sup

added theorem subsemigroup.map_sup_comap_of_surjective

added theorem subsemigroup.map_supr

added theorem subsemigroup.map_supr_comap_of_surjective

added theorem subsemigroup.map_surjective_of_surjective

added theorem subsemigroup.mem_comap

added theorem subsemigroup.mem_map

added theorem subsemigroup.mem_map_equiv

added theorem subsemigroup.mem_map_iff_mem

added theorem subsemigroup.mem_map_of_mem

added theorem subsemigroup.mem_prod

added theorem subsemigroup.monotone_comap

added theorem subsemigroup.monotone_map

added def subsemigroup.prod

added theorem subsemigroup.prod_eq_top_iff

added def subsemigroup.prod_equiv

added theorem subsemigroup.prod_mono

added theorem subsemigroup.prod_top

added theorem subsemigroup.range_subtype

added theorem subsemigroup.srange_fst

added theorem subsemigroup.srange_snd

added def subsemigroup.to_add_subsemigroup'

added theorem subsemigroup.to_add_subsemigroup'_closure

added def subsemigroup.to_add_subsemigroup

added theorem subsemigroup.to_add_subsemigroup_closure

added def subsemigroup.top_equiv

added theorem subsemigroup.top_equiv_to_mul_hom

added theorem subsemigroup.top_prod

added theorem subsemigroup.top_prod_top