Commit 2023-04-14 23:46 c7c0f547

View on Github →

feat: Port RingTheory.NonUnitalSubsemiring.Basic (#1774)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/Subsemigroup/Center.lean

Created Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

added def NonUnitalRingHom.codRestrict

added theorem NonUnitalRingHom.coe_srange

added theorem NonUnitalRingHom.coe_srangeRestrict

added theorem NonUnitalRingHom.eqOn_sclosure

added def NonUnitalRingHom.eqSlocus

added theorem NonUnitalRingHom.eq_of_eqOn_sdense

added theorem NonUnitalRingHom.eq_of_eqOn_stop

added theorem NonUnitalRingHom.map_sclosure

added theorem NonUnitalRingHom.map_srange

added theorem NonUnitalRingHom.mem_srange

added theorem NonUnitalRingHom.mem_srange_self

added theorem NonUnitalRingHom.sclosure_preimage_le

added def NonUnitalRingHom.srange

added def NonUnitalRingHom.srangeRestrict

added theorem NonUnitalRingHom.srangeRestrict_surjective

added theorem NonUnitalRingHom.srange_eq_map

added theorem NonUnitalRingHom.srange_top_iff_surjective

added theorem NonUnitalRingHom.srange_top_of_surjective

added def NonUnitalSubsemiring.center

added theorem NonUnitalSubsemiring.center_eq_top

added theorem NonUnitalSubsemiring.center_toSubsemigroup

added def NonUnitalSubsemiring.centralizer

added theorem NonUnitalSubsemiring.centralizer_le

added theorem NonUnitalSubsemiring.centralizer_toSubsemigroup

added theorem NonUnitalSubsemiring.centralizer_univ

added def NonUnitalSubsemiring.closure

added theorem NonUnitalSubsemiring.closure_addSubmonoid_closure

added theorem NonUnitalSubsemiring.closure_empty

added theorem NonUnitalSubsemiring.closure_eq

added theorem NonUnitalSubsemiring.closure_eq_of_le

added theorem NonUnitalSubsemiring.closure_induction

added theorem NonUnitalSubsemiring.closure_induction₂

added theorem NonUnitalSubsemiring.closure_le

added theorem NonUnitalSubsemiring.closure_mono

added theorem NonUnitalSubsemiring.closure_subsemigroup_closure

added theorem NonUnitalSubsemiring.closure_union

added theorem NonUnitalSubsemiring.closure_unionᵢ

added theorem NonUnitalSubsemiring.closure_unionₛ

added theorem NonUnitalSubsemiring.closure_univ

added theorem NonUnitalSubsemiring.coe_add

added theorem NonUnitalSubsemiring.coe_bot

added theorem NonUnitalSubsemiring.coe_center

added theorem NonUnitalSubsemiring.coe_centralizer

added theorem NonUnitalSubsemiring.coe_closure_eq

added theorem NonUnitalSubsemiring.coe_comap

added theorem NonUnitalSubsemiring.coe_copy

added theorem NonUnitalSubsemiring.coe_equivMapOfInjective_apply

added theorem NonUnitalSubsemiring.coe_inf

added theorem NonUnitalSubsemiring.coe_infₛ

added theorem NonUnitalSubsemiring.coe_map

added theorem NonUnitalSubsemiring.coe_mk'

added theorem NonUnitalSubsemiring.coe_mul

added theorem NonUnitalSubsemiring.coe_prod

added theorem NonUnitalSubsemiring.coe_supᵢ_of_directed

added theorem NonUnitalSubsemiring.coe_supₛ_of_directedOn

added theorem NonUnitalSubsemiring.coe_toAddSubmonoid

added theorem NonUnitalSubsemiring.coe_toSubsemigroup

added theorem NonUnitalSubsemiring.coe_top

added theorem NonUnitalSubsemiring.coe_zero

added def NonUnitalSubsemiring.comap

added theorem NonUnitalSubsemiring.comap_comap

added theorem NonUnitalSubsemiring.comap_equiv_eq_map_symm

added theorem NonUnitalSubsemiring.comap_inf

added theorem NonUnitalSubsemiring.comap_infᵢ

added theorem NonUnitalSubsemiring.comap_top

added theorem NonUnitalSubsemiring.copy_eq

added theorem NonUnitalSubsemiring.eq_top_iff'

added theorem NonUnitalSubsemiring.ext

added theorem NonUnitalSubsemiring.gc_map_comap

added def NonUnitalSubsemiring.inclusion

added theorem NonUnitalSubsemiring.infₛ_toAddSubmonoid

added theorem NonUnitalSubsemiring.infₛ_toSubsemigroup

added def NonUnitalSubsemiring.map

added theorem NonUnitalSubsemiring.map_bot

added theorem NonUnitalSubsemiring.map_equiv_eq_comap_symm

added theorem NonUnitalSubsemiring.map_id

added theorem NonUnitalSubsemiring.map_le_iff_le_comap

added theorem NonUnitalSubsemiring.map_map

added theorem NonUnitalSubsemiring.map_sup

added theorem NonUnitalSubsemiring.map_supᵢ

added theorem NonUnitalSubsemiring.mem_bot

added theorem NonUnitalSubsemiring.mem_carrier

added theorem NonUnitalSubsemiring.mem_center_iff

added theorem NonUnitalSubsemiring.mem_centralizer_iff

added theorem NonUnitalSubsemiring.mem_closure

added theorem NonUnitalSubsemiring.mem_closure_iff

added theorem NonUnitalSubsemiring.mem_comap

added theorem NonUnitalSubsemiring.mem_inf

added theorem NonUnitalSubsemiring.mem_infₛ

added theorem NonUnitalSubsemiring.mem_map

added theorem NonUnitalSubsemiring.mem_map_equiv

added theorem NonUnitalSubsemiring.mem_mk'

added theorem NonUnitalSubsemiring.mem_prod

added theorem NonUnitalSubsemiring.mem_supᵢ_of_directed

added theorem NonUnitalSubsemiring.mem_supₛ_of_directedOn

added theorem NonUnitalSubsemiring.mem_toAddSubmonoid

added theorem NonUnitalSubsemiring.mem_toSubsemigroup

added theorem NonUnitalSubsemiring.mem_top

added theorem NonUnitalSubsemiring.mk'_toAddSubmonoid

added theorem NonUnitalSubsemiring.mk'_toSubsemigroup

added theorem NonUnitalSubsemiring.not_mem_of_not_mem_closure

added def NonUnitalSubsemiring.prod

added def NonUnitalSubsemiring.prodEquiv

added theorem NonUnitalSubsemiring.prod_mono

added theorem NonUnitalSubsemiring.prod_mono_left

added theorem NonUnitalSubsemiring.prod_mono_right

added theorem NonUnitalSubsemiring.prod_top

added theorem NonUnitalSubsemiring.range_fst

added theorem NonUnitalSubsemiring.range_snd

added theorem NonUnitalSubsemiring.srange_subtype

added theorem NonUnitalSubsemiring.subset_closure

added theorem NonUnitalSubsemiring.toAddSubmonoid_injective

added theorem NonUnitalSubsemiring.toAddSubmonoid_mono

added theorem NonUnitalSubsemiring.toAddSubmonoid_strictMono

added theorem NonUnitalSubsemiring.toSubsemigroup_injective

added theorem NonUnitalSubsemiring.toSubsemigroup_mono

added theorem NonUnitalSubsemiring.toSubsemigroup_strictMono

added theorem NonUnitalSubsemiring.top_prod

added theorem NonUnitalSubsemiring.top_prod_top

added structure NonUnitalSubsemiring

added theorem NonUnitalSubsemiringClass.coeSubtype

added def NonUnitalSubsemiringClass.subtype

added def RingEquiv.nonUnitalSubsemiringCongr

added def RingEquiv.nonUnitalSubsemiringMap

added def RingEquiv.sofLeftInverse'

added theorem RingEquiv.sofLeftInverse'_apply

added theorem RingEquiv.sofLeftInverse'_symm_apply

added def Subsemigroup.nonUnitalSubsemiringClosure

added theorem Subsemigroup.nonUnitalSubsemiringClosure_coe

added theorem Subsemigroup.nonUnitalSubsemiringClosure_eq_closure

added theorem Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid