Commit 2024-11-04 05:25 7abccc07

View on Github →

chore(RingTheory/NonUnitalSubring): split Basic.lean (#18518) This PR splits off a Defs.lean file from NonUnitalSubring/Basic.lean containing on the definition and non unital subring structure of NonUnitalSubring(Class).

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Ring/Subring/Basic.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/RingTheory/NonUnitalSubring/Basic.lean

deleted theorem NonUnitalSubring.coe_copy

deleted theorem NonUnitalSubring.coe_eq_zero_iff

deleted theorem NonUnitalSubring.coe_mk'

deleted theorem NonUnitalSubring.coe_set_mk

deleted theorem NonUnitalSubring.coe_toAddSubgroup

deleted theorem NonUnitalSubring.coe_toNonUnitalSubsemiring

deleted theorem NonUnitalSubring.coe_toSubsemigroup

deleted theorem NonUnitalSubring.copy_eq

deleted theorem NonUnitalSubring.ext

deleted def NonUnitalSubring.inclusion

deleted theorem NonUnitalSubring.mem_carrier

deleted theorem NonUnitalSubring.mem_mk'

deleted theorem NonUnitalSubring.mem_mk

deleted theorem NonUnitalSubring.mem_toAddSubgroup

deleted theorem NonUnitalSubring.mem_toNonUnitalSubsemiring

deleted theorem NonUnitalSubring.mem_toSubsemigroup

deleted theorem NonUnitalSubring.mk'_toAddSubgroup

deleted theorem NonUnitalSubring.mk'_toSubsemigroup

deleted theorem NonUnitalSubring.mk_le_mk

deleted theorem NonUnitalSubring.toAddSubgroup_injective

deleted theorem NonUnitalSubring.toAddSubgroup_mono

deleted theorem NonUnitalSubring.toAddSubgroup_strictMono

deleted theorem NonUnitalSubring.toNonUnitalSubsemiring_injective

deleted theorem NonUnitalSubring.toNonUnitalSubsemiring_mono

deleted theorem NonUnitalSubring.toNonUnitalSubsemiring_strictMono

deleted def NonUnitalSubring.toSubsemigroup

deleted theorem NonUnitalSubring.toSubsemigroup_injective

deleted theorem NonUnitalSubring.toSubsemigroup_mono

deleted theorem NonUnitalSubring.toSubsemigroup_strictMono

deleted theorem NonUnitalSubring.val_add

deleted theorem NonUnitalSubring.val_mul

deleted theorem NonUnitalSubring.val_neg

deleted theorem NonUnitalSubring.val_zero

deleted structure NonUnitalSubring

deleted theorem NonUnitalSubringClass.coe_subtype

deleted def NonUnitalSubringClass.subtype

Created Mathlib/RingTheory/NonUnitalSubring/Defs.lean

added theorem NonUnitalSubring.coe_copy

added theorem NonUnitalSubring.coe_eq_zero_iff

added theorem NonUnitalSubring.coe_mk'

added theorem NonUnitalSubring.coe_set_mk

added theorem NonUnitalSubring.coe_toAddSubgroup

added theorem NonUnitalSubring.coe_toNonUnitalSubsemiring

added theorem NonUnitalSubring.coe_toSubsemigroup

added theorem NonUnitalSubring.copy_eq

added theorem NonUnitalSubring.ext

added def NonUnitalSubring.inclusion

added theorem NonUnitalSubring.mem_carrier

added theorem NonUnitalSubring.mem_mk'

added theorem NonUnitalSubring.mem_mk

added theorem NonUnitalSubring.mem_toAddSubgroup

added theorem NonUnitalSubring.mem_toNonUnitalSubsemiring

added theorem NonUnitalSubring.mem_toSubsemigroup

added theorem NonUnitalSubring.mk'_toAddSubgroup

added theorem NonUnitalSubring.mk'_toSubsemigroup

added theorem NonUnitalSubring.mk_le_mk

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 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

Modified Mathlib/RingTheory/TwoSidedIdeal/Instances.lean