Commit 2024-11-03 08:14 2d1f8f40

View on Github →

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

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

deleted def NonUnitalRingHom.codRestrict

deleted def NonUnitalRingHom.eqSlocus

deleted theorem NonUnitalSubsemiring.coe_add

deleted theorem NonUnitalSubsemiring.coe_bot

deleted theorem NonUnitalSubsemiring.coe_copy

deleted theorem NonUnitalSubsemiring.coe_inf

deleted theorem NonUnitalSubsemiring.coe_mk'

deleted theorem NonUnitalSubsemiring.coe_mul

deleted theorem NonUnitalSubsemiring.coe_toAddSubmonoid

deleted theorem NonUnitalSubsemiring.coe_toSubsemigroup

deleted theorem NonUnitalSubsemiring.coe_top

deleted theorem NonUnitalSubsemiring.coe_zero

deleted theorem NonUnitalSubsemiring.copy_eq

deleted theorem NonUnitalSubsemiring.ext

deleted def NonUnitalSubsemiring.inclusion

deleted theorem NonUnitalSubsemiring.mem_bot

deleted theorem NonUnitalSubsemiring.mem_carrier

deleted theorem NonUnitalSubsemiring.mem_inf

deleted theorem NonUnitalSubsemiring.mem_mk'

deleted theorem NonUnitalSubsemiring.mem_toAddSubmonoid

deleted theorem NonUnitalSubsemiring.mem_toSubsemigroup

deleted theorem NonUnitalSubsemiring.mem_top

deleted theorem NonUnitalSubsemiring.mk'_toAddSubmonoid

deleted theorem NonUnitalSubsemiring.mk'_toSubsemigroup

deleted theorem NonUnitalSubsemiring.toAddSubmonoid_injective

deleted theorem NonUnitalSubsemiring.toSubsemigroup_injective

deleted structure NonUnitalSubsemiring

deleted theorem NonUnitalSubsemiringClass.coeSubtype

deleted def NonUnitalSubsemiringClass.subtype

Created Mathlib/RingTheory/NonUnitalSubsemiring/Defs.lean

added def NonUnitalRingHom.codRestrict

added def NonUnitalRingHom.eqSlocus

added theorem NonUnitalSubsemiring.coe_add

added theorem NonUnitalSubsemiring.coe_bot

added theorem NonUnitalSubsemiring.coe_copy

added theorem NonUnitalSubsemiring.coe_inf

added theorem NonUnitalSubsemiring.coe_mk'

added theorem NonUnitalSubsemiring.coe_mul

added theorem NonUnitalSubsemiring.coe_toAddSubmonoid

added theorem NonUnitalSubsemiring.coe_toSubsemigroup

added theorem NonUnitalSubsemiring.coe_top

added theorem NonUnitalSubsemiring.coe_zero

added theorem NonUnitalSubsemiring.copy_eq

added theorem NonUnitalSubsemiring.ext

added def NonUnitalSubsemiring.inclusion

added theorem NonUnitalSubsemiring.mem_bot

added theorem NonUnitalSubsemiring.mem_carrier

added theorem NonUnitalSubsemiring.mem_inf

added theorem NonUnitalSubsemiring.mem_mk'

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

added theorem NonUnitalSubsemiring.toSubsemigroup_injective

added structure NonUnitalSubsemiring

added theorem NonUnitalSubsemiringClass.coeSubtype

added def NonUnitalSubsemiringClass.subtype