Commit 2023-01-30 11:31 3079782f

View on Github →

feat: port RingTheory.Subsemiring.Basic (#1862)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/Submonoid/Center.lean

Modified Mathlib/GroupTheory/Submonoid/Operations.lean

Modified Mathlib/Order/Directed.lean

modified theorem Directed.mono_comp

Created Mathlib/RingTheory/Subsemiring/Basic.lean

added def RingEquiv.ofLeftInverseS

added theorem RingEquiv.ofLeftInverseS_apply

added theorem RingEquiv.ofLeftInverseS_symm_apply

added def RingEquiv.subsemiringCongr

added def RingEquiv.subsemiringMap

added def RingHom.codRestrict

added theorem RingHom.coe_rangeS

added theorem RingHom.coe_rangeSRestrict

added theorem RingHom.coe_restrict_apply

added theorem RingHom.comp_restrict

added def RingHom.domRestrict

added def RingHom.eqLocusS

added theorem RingHom.eqLocusS_same

added theorem RingHom.eqOn_sclosure

added theorem RingHom.eq_of_eqOn_sdense

added theorem RingHom.eq_of_eqOn_stop

added theorem RingHom.map_closureS

added theorem RingHom.map_rangeS

added theorem RingHom.mem_rangeS

added theorem RingHom.mem_rangeS_self

added def RingHom.rangeS

added def RingHom.rangeSRestrict

added theorem RingHom.rangeSRestrict_surjective

added theorem RingHom.rangeS_eq_map

added theorem RingHom.rangeS_top_iff_surjective

added theorem RingHom.rangeS_top_of_surjective

added def RingHom.restrict

added theorem RingHom.restrict_apply

added theorem RingHom.sclosure_preimage_le

added def Submonoid.subsemiringClosure

added theorem Submonoid.subsemiringClosure_coe

added theorem Submonoid.subsemiringClosure_eq_closure

added theorem Submonoid.subsemiringClosure_toAddSubmonoid

added def Subsemiring.center

added theorem Subsemiring.center_eq_top

added theorem Subsemiring.center_toSubmonoid

added def Subsemiring.centralizer

added theorem Subsemiring.centralizer_le

added theorem Subsemiring.centralizer_toSubmonoid

added theorem Subsemiring.centralizer_univ

added def Subsemiring.closure

added def Subsemiring.closureCommSemiringOfComm

added theorem Subsemiring.closure_addSubmonoid_closure

added theorem Subsemiring.closure_empty

added theorem Subsemiring.closure_eq

added theorem Subsemiring.closure_eq_of_le

added theorem Subsemiring.closure_induction

added theorem Subsemiring.closure_induction₂

added theorem Subsemiring.closure_le

added theorem Subsemiring.closure_mono

added theorem Subsemiring.closure_submonoid_closure

added theorem Subsemiring.closure_union

added theorem Subsemiring.closure_unionᵢ

added theorem Subsemiring.closure_unionₛ

added theorem Subsemiring.closure_univ

added theorem Subsemiring.coe_add

added theorem Subsemiring.coe_bot

added theorem Subsemiring.coe_carrier_toSubmonoid

added theorem Subsemiring.coe_center

added theorem Subsemiring.coe_centralizer

added theorem Subsemiring.coe_closure_eq

added theorem Subsemiring.coe_comap

added theorem Subsemiring.coe_copy

added theorem Subsemiring.coe_equivMapOfInjective_apply

added theorem Subsemiring.coe_inf

added theorem Subsemiring.coe_infₛ

added theorem Subsemiring.coe_map

added theorem Subsemiring.coe_mk'

added theorem Subsemiring.coe_mul

added theorem Subsemiring.coe_one

added theorem Subsemiring.coe_pow

added theorem Subsemiring.coe_prod

added theorem Subsemiring.coe_subtype

added theorem Subsemiring.coe_supᵢ_of_directed

added theorem Subsemiring.coe_supₛ_of_directedOn

added theorem Subsemiring.coe_toAddSubmonoid

added theorem Subsemiring.coe_toSubmonoid

added theorem Subsemiring.coe_top

added theorem Subsemiring.coe_zero

added def Subsemiring.comap

added theorem Subsemiring.comap_comap

added theorem Subsemiring.comap_equiv_eq_map_symm

added theorem Subsemiring.comap_inf

added theorem Subsemiring.comap_infᵢ

added theorem Subsemiring.comap_top

added theorem Subsemiring.copy_eq

added theorem Subsemiring.eq_top_iff'

added theorem Subsemiring.ext

added theorem Subsemiring.gc_map_comap

added def Subsemiring.inclusion

added theorem Subsemiring.infₛ_toAddSubmonoid

added theorem Subsemiring.infₛ_toSubmonoid

added def Subsemiring.map

added theorem Subsemiring.map_bot

added theorem Subsemiring.map_equiv_eq_comap_symm

added theorem Subsemiring.map_id

added theorem Subsemiring.map_le_iff_le_comap

added theorem Subsemiring.map_map

added theorem Subsemiring.map_sup

added theorem Subsemiring.map_supᵢ

added theorem Subsemiring.mem_bot

added theorem Subsemiring.mem_carrier

added theorem Subsemiring.mem_center_iff

added theorem Subsemiring.mem_centralizer_iff

added theorem Subsemiring.mem_closure

added theorem Subsemiring.mem_closure_iff

added theorem Subsemiring.mem_closure_iff_exists_list

added theorem Subsemiring.mem_comap

added theorem Subsemiring.mem_inf

added theorem Subsemiring.mem_infₛ

added theorem Subsemiring.mem_map

added theorem Subsemiring.mem_map_equiv

added theorem Subsemiring.mem_mk'

added theorem Subsemiring.mem_prod

added theorem Subsemiring.mem_supᵢ_of_directed

added theorem Subsemiring.mem_supₛ_of_directedOn

added theorem Subsemiring.mem_toAddSubmonoid

added theorem Subsemiring.mem_toSubmonoid

added theorem Subsemiring.mem_top

added theorem Subsemiring.mk'_toAddSubmonoid

added theorem Subsemiring.mk'_toSubmonoid

added theorem Subsemiring.not_mem_of_not_mem_closure

added def Subsemiring.prod

added def Subsemiring.prodEquiv

added theorem Subsemiring.prod_bot_sup_bot_prod

added theorem Subsemiring.prod_mono

added theorem Subsemiring.prod_mono_left

added theorem Subsemiring.prod_mono_right

added theorem Subsemiring.prod_top

added theorem Subsemiring.rangeS_subtype

added theorem Subsemiring.range_fst

added theorem Subsemiring.range_snd

added theorem Subsemiring.smul_def

added theorem Subsemiring.subset_closure

added def Subsemiring.subtype

added theorem Subsemiring.toAddSubmonoid_injective

added theorem Subsemiring.toAddSubmonoid_mono

added theorem Subsemiring.toAddSubmonoid_strictMono

added theorem Subsemiring.toSubmonoid_injective

added theorem Subsemiring.toSubmonoid_mono

added theorem Subsemiring.toSubmonoid_strictMono

added def Subsemiring.topEquiv

added theorem Subsemiring.top_prod

added theorem Subsemiring.top_prod_top

added structure Subsemiring

added theorem SubsemiringClass.coe_pow

added theorem SubsemiringClass.coe_subtype

added def SubsemiringClass.subtype

added theorem coe_nat_mem

added theorem mem_posSubmonoid

added theorem natCast_mem

added def posSubmonoid