Commit 2023-01-17 15:34 ea14e3c7

View on Github →

feat: port RingTheory.Congruence (#1629)

Estimated changes

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 structure RingCon
added inductive RingConGen.Rel
added def ringConGen