Commit 2021-08-19 15:14 84271fe0

View on Github →

CommRing ℤ instance (#40)

feat : instance Z CommRing
fix : typo SubNegMonoid
fix : unnecessary lemma

Estimated changes

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/Ring/Basic.lean

added theorem Int.ofNat_eq_ofNat