Commit 2022-12-31 09:21 1e1ba1eb

View on Github →

feat: port GroupTheory.Subsemigroup.Operations (#1235)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/Subsemigroup/Basic.lean

Created Mathlib/GroupTheory/Subsemigroup/Operations.lean

added theorem AddSubsemigroup.toSubsemigroup'_closure

added def AddSubsemigroup.toSubsemigroup

added theorem AddSubsemigroup.toSubsemigroup_closure

added def MulEquiv.ofLeftInverse

added def MulEquiv.subsemigroupCongr

added def MulEquiv.subsemigroupMap

added def MulHom.codRestrict

added theorem MulHom.coe_srange

added theorem MulHom.coe_srangeRestrict

added theorem MulHom.map_mclosure

added theorem MulHom.map_srange

added theorem MulHom.mclosure_preimage_le

added theorem MulHom.mem_srange

added theorem MulHom.prod_map_comap_prod'

added def MulHom.restrict

added theorem MulHom.restrict_apply

added def MulHom.srange

added def MulHom.srangeRestrict

added theorem MulHom.srangeRestrict_surjective

added theorem MulHom.srange_eq_map

added theorem MulHom.srange_top_iff_surjective

added theorem MulHom.srange_top_of_surjective

added def MulHom.subsemigroupComap

added def MulHom.subsemigroupMap

added theorem MulHom.subsemigroupMap_surjective

added theorem MulMemClass.coe_mul

added theorem MulMemClass.coe_subtype

added theorem MulMemClass.mk_mul_mk

added theorem MulMemClass.mul_def

added def MulMemClass.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_equivMapOfInjective_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_infᵢ

added theorem Subsemigroup.comap_infᵢ_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_strictMono_of_surjective

added theorem Subsemigroup.comap_sup_map_of_injective

added theorem Subsemigroup.comap_supᵢ_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.gciMapComap

added def Subsemigroup.giMapComap

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_infᵢ_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_strictMono_of_injective

added theorem Subsemigroup.map_sup

added theorem Subsemigroup.map_sup_comap_of_surjective

added theorem Subsemigroup.map_supᵢ

added theorem Subsemigroup.map_supᵢ_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 def Subsemigroup.prodEquiv

added theorem Subsemigroup.prod_eq_top_iff

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 theorem Subsemigroup.toAddSubsemigroup'_closure

added def Subsemigroup.toAddSubsemigroup

added theorem Subsemigroup.toAddSubsemigroup_closure

added def Subsemigroup.topEquiv

added theorem Subsemigroup.topEquiv_toMulHom

added theorem Subsemigroup.top_prod

added theorem Subsemigroup.top_prod_top