Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-01-17 15:34
ea14e3c7
View on Github →
feat: port RingTheory.Congruence (
#1629
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/RingTheory/Congruence.lean
added
theorem
RingCon.coe_add
added
theorem
RingCon.coe_int_cast
added
theorem
RingCon.coe_mul
added
theorem
RingCon.coe_nat_cast
added
theorem
RingCon.coe_neg
added
theorem
RingCon.coe_nsmul
added
theorem
RingCon.coe_one
added
theorem
RingCon.coe_pow
added
theorem
RingCon.coe_smul
added
theorem
RingCon.coe_sub
added
theorem
RingCon.coe_zero
added
theorem
RingCon.coe_zsmul
added
def
RingCon.mk'
added
theorem
RingCon.quot_mk_eq_coe
added
theorem
RingCon.rel_eq_coe
added
theorem
RingCon.rel_mk
added
def
RingCon.toAddCon
added
def
RingCon.toCon
added
def
RingCon.toQuotient
added
structure
RingCon
added
inductive
RingConGen.Rel
added
def
ringConGen