Commit 2024-10-29 15:17 f4f0b47a

View on Github →

chore(RingTheory/Congruence): split off Defs.lean (#18387) The goal of this PR is to split off enough to define the ideal quotient and its ring structure without too much theory in the way.

Estimated changes

deleted theorem RingCon.coe_add
deleted theorem RingCon.coe_intCast
deleted theorem RingCon.coe_mul
deleted theorem RingCon.coe_natCast
deleted theorem RingCon.coe_neg
deleted theorem RingCon.coe_nsmul
deleted theorem RingCon.coe_one
deleted theorem RingCon.coe_pow
deleted theorem RingCon.coe_sub
deleted theorem RingCon.coe_zero
deleted theorem RingCon.coe_zsmul
deleted def RingCon.comap
deleted theorem RingCon.ext'
deleted theorem RingCon.ext
deleted def RingCon.mk'
deleted theorem RingCon.quot_mk_eq_coe
deleted theorem RingCon.rel_eq_coe
deleted theorem RingCon.rel_mk
deleted theorem RingCon.toCon_coe_eq_coe
deleted def RingCon.toQuotient
deleted structure RingCon
deleted inductive RingConGen.Rel
deleted def ringConGen
added theorem RingCon.coe_add
added theorem RingCon.coe_intCast
added theorem RingCon.coe_mul
added theorem RingCon.coe_natCast
added theorem RingCon.coe_neg
added theorem RingCon.coe_nsmul
added theorem RingCon.coe_one
added theorem RingCon.coe_pow
added theorem RingCon.coe_sub
added theorem RingCon.coe_zero
added theorem RingCon.coe_zsmul
added def RingCon.comap
added theorem RingCon.ext'
added theorem RingCon.ext
added def RingCon.mk'
added theorem RingCon.quot_mk_eq_coe
added theorem RingCon.rel_eq_coe
added theorem RingCon.rel_mk
added structure RingCon
added inductive RingConGen.Rel
added def ringConGen