Commit 2024-11-03 19:16 ddfa45d2

View on Github →

chore(Algebra/Ring/Subsemiring): split Basic.lean (#18519) This PR splits off a Defs.lean file from Subsemiring/Basic.lean containing on the definition and subsemiring structure of Subsemiring(Class).

Estimated changes

deleted def RingHom.domRestrict
deleted def RingHom.eqLocusS
deleted theorem RingHom.eqLocusS_same
deleted theorem RingHom.restrict_apply
deleted theorem Subsemiring.coe_add
deleted theorem Subsemiring.coe_copy
deleted theorem Subsemiring.coe_inf
deleted theorem Subsemiring.coe_mk'
deleted theorem Subsemiring.coe_mul
deleted theorem Subsemiring.coe_one
deleted theorem Subsemiring.coe_pow
deleted theorem Subsemiring.coe_subtype
deleted theorem Subsemiring.coe_top
deleted theorem Subsemiring.coe_zero
deleted theorem Subsemiring.copy_eq
deleted theorem Subsemiring.ext
deleted theorem Subsemiring.mem_carrier
deleted theorem Subsemiring.mem_inf
deleted theorem Subsemiring.mem_mk'
deleted theorem Subsemiring.mem_top
deleted def Subsemiring.subtype
deleted structure Subsemiring
deleted theorem SubsemiringClass.coe_pow
deleted theorem natCast_mem
deleted theorem ofNat_mem
added def RingHom.eqLocusS
added theorem RingHom.eqLocusS_same
added theorem RingHom.restrict_apply
added theorem Subsemiring.coe_add
added theorem Subsemiring.coe_copy
added theorem Subsemiring.coe_inf
added theorem Subsemiring.coe_mk'
added theorem Subsemiring.coe_mul
added theorem Subsemiring.coe_one
added theorem Subsemiring.coe_pow
added theorem Subsemiring.coe_top
added theorem Subsemiring.coe_zero
added theorem Subsemiring.copy_eq
added theorem Subsemiring.ext
added theorem Subsemiring.mem_inf
added theorem Subsemiring.mem_mk'
added theorem Subsemiring.mem_top
added structure Subsemiring
added theorem natCast_mem
added theorem ofNat_mem