Commit 2023-07-01 15:01 d512093b

View on Github →

feat: define NonUnitalSubrings (#5151) This continues the non-unital-ization of mathlib by defining NonUnitalSubring. We attempt to provide as much feature parity as possible with both NonUnitalSubsemiring and Subring.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/Subsemigroup/Center.lean

modified theorem Set.neg_mem_center

Created Mathlib/RingTheory/NonUnitalSubring/Basic.lean

added theorem NonUnitalRingHom.closure_preimage_le

added theorem NonUnitalRingHom.coe_range

added theorem NonUnitalRingHom.coe_rangeRestrict

added def NonUnitalRingHom.eqLocus

added theorem NonUnitalRingHom.eqLocus_same

added theorem NonUnitalRingHom.eqOn_set_closure

added theorem NonUnitalRingHom.eq_of_eqOn_set_dense

added theorem NonUnitalRingHom.eq_of_eqOn_set_top

added theorem NonUnitalRingHom.map_closure

added theorem NonUnitalRingHom.map_range

added theorem NonUnitalRingHom.mem_range

added theorem NonUnitalRingHom.mem_range_self

added def NonUnitalRingHom.range

added def NonUnitalRingHom.rangeRestrict

added theorem NonUnitalRingHom.rangeRestrict_surjective

added theorem NonUnitalRingHom.range_eq_map

added theorem NonUnitalRingHom.range_top_iff_surjective

added theorem NonUnitalRingHom.range_top_of_surjective

added def NonUnitalSubring.center

added theorem NonUnitalSubring.center_eq_top

added theorem NonUnitalSubring.center_toNonUnitalSubsemiring

added def NonUnitalSubring.closure

added def NonUnitalSubring.closureNonUnitalCommRingOfComm

added theorem NonUnitalSubring.closure_empty

added theorem NonUnitalSubring.closure_eq

added theorem NonUnitalSubring.closure_eq_of_le

added theorem NonUnitalSubring.closure_iUnion

added theorem NonUnitalSubring.closure_induction'

added theorem NonUnitalSubring.closure_induction

added theorem NonUnitalSubring.closure_induction₂

added theorem NonUnitalSubring.closure_le

added theorem NonUnitalSubring.closure_mono

added theorem NonUnitalSubring.closure_preimage_le

added theorem NonUnitalSubring.closure_sUnion

added theorem NonUnitalSubring.closure_union

added theorem NonUnitalSubring.closure_univ

added theorem NonUnitalSubring.coe_bot

added theorem NonUnitalSubring.coe_center

added theorem NonUnitalSubring.coe_comap

added theorem NonUnitalSubring.coe_copy

added theorem NonUnitalSubring.coe_eq_zero_iff

added theorem NonUnitalSubring.coe_equivMapOfInjective_apply

added theorem NonUnitalSubring.coe_iInf

added theorem NonUnitalSubring.coe_iSup_of_directed

added theorem NonUnitalSubring.coe_inf

added theorem NonUnitalSubring.coe_map

added theorem NonUnitalSubring.coe_mk'

added theorem NonUnitalSubring.coe_prod

added theorem NonUnitalSubring.coe_sInf

added theorem NonUnitalSubring.coe_sSup_of_directedOn

added theorem NonUnitalSubring.coe_set_mk

added theorem NonUnitalSubring.coe_toAddSubgroup

added theorem NonUnitalSubring.coe_toNonUnitalSubsemiring

added theorem NonUnitalSubring.coe_toSubsemigroup

added theorem NonUnitalSubring.coe_top

added def NonUnitalSubring.comap

added theorem NonUnitalSubring.comap_comap

added theorem NonUnitalSubring.comap_equiv_eq_map_symm

added theorem NonUnitalSubring.comap_iInf

added theorem NonUnitalSubring.comap_inf

added theorem NonUnitalSubring.comap_top

added theorem NonUnitalSubring.copy_eq

added theorem NonUnitalSubring.eq_top_iff'

added theorem NonUnitalSubring.ext

added theorem NonUnitalSubring.gc_map_comap

added def NonUnitalSubring.inclusion

added def NonUnitalSubring.map

added theorem NonUnitalSubring.map_bot

added theorem NonUnitalSubring.map_equiv_eq_comap_symm

added theorem NonUnitalSubring.map_iSup

added theorem NonUnitalSubring.map_id

added theorem NonUnitalSubring.map_le_iff_le_comap

added theorem NonUnitalSubring.map_map

added theorem NonUnitalSubring.map_sup

added theorem NonUnitalSubring.mem_bot

added theorem NonUnitalSubring.mem_carrier

added theorem NonUnitalSubring.mem_center_iff

added theorem NonUnitalSubring.mem_closure

added theorem NonUnitalSubring.mem_closure_iff

added theorem NonUnitalSubring.mem_comap

added theorem NonUnitalSubring.mem_iInf

added theorem NonUnitalSubring.mem_iSup_of_directed

added theorem NonUnitalSubring.mem_inf

added theorem NonUnitalSubring.mem_map

added theorem NonUnitalSubring.mem_map_equiv

added theorem NonUnitalSubring.mem_mk'

added theorem NonUnitalSubring.mem_mk

added theorem NonUnitalSubring.mem_prod

added theorem NonUnitalSubring.mem_sInf

added theorem NonUnitalSubring.mem_sSup_of_directedOn

added theorem NonUnitalSubring.mem_toAddSubgroup

added theorem NonUnitalSubring.mem_toNonUnitalSubsemiring

added theorem NonUnitalSubring.mem_toSubsemigroup

added theorem NonUnitalSubring.mem_top

added theorem NonUnitalSubring.mk'_toAddSubgroup

added theorem NonUnitalSubring.mk'_toSubsemigroup

added theorem NonUnitalSubring.mk_le_mk

added theorem NonUnitalSubring.not_mem_of_not_mem_closure

added def NonUnitalSubring.prod

added def NonUnitalSubring.prodEquiv

added theorem NonUnitalSubring.prod_mono

added theorem NonUnitalSubring.prod_mono_left

added theorem NonUnitalSubring.prod_mono_right

added theorem NonUnitalSubring.prod_top

added theorem NonUnitalSubring.range_fst

added theorem NonUnitalSubring.range_snd

added theorem NonUnitalSubring.range_subtype

added theorem NonUnitalSubring.sInf_toAddSubgroup

added theorem NonUnitalSubring.sInf_toSubsemigroup

added theorem NonUnitalSubring.subset_closure

added theorem NonUnitalSubring.toAddSubgroup_injective

added theorem NonUnitalSubring.toAddSubgroup_mono

added theorem NonUnitalSubring.toAddSubgroup_strictMono

added theorem NonUnitalSubring.toNonUnitalSubsemiring_injective

added theorem NonUnitalSubring.toNonUnitalSubsemiring_mono

added theorem NonUnitalSubring.toNonUnitalSubsemiring_strictMono

added def NonUnitalSubring.toSubsemigroup

added theorem NonUnitalSubring.toSubsemigroup_injective

added theorem NonUnitalSubring.toSubsemigroup_mono

added theorem NonUnitalSubring.toSubsemigroup_strictMono

added def NonUnitalSubring.topEquiv

added theorem NonUnitalSubring.top_prod

added theorem NonUnitalSubring.top_prod_top

added theorem NonUnitalSubring.val_add

added theorem NonUnitalSubring.val_mul

added theorem NonUnitalSubring.val_neg

added theorem NonUnitalSubring.val_zero

added structure NonUnitalSubring

added theorem NonUnitalSubringClass.coe_subtype

added def NonUnitalSubringClass.subtype

added def RingEquiv.nonUnitalSubringCongr

added def RingEquiv.ofLeftInverse'

added theorem RingEquiv.ofLeftInverse'_apply

added theorem RingEquiv.ofLeftInverse'_symm_apply

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

modified def NonUnitalRingHom.codRestrict

added def NonUnitalSubsemiring.topEquiv