diff --git a/Mathlib/Algebra/RingQuot.lean b/Mathlib/Algebra/RingQuot.lean index 4a9c6d387ec04..4faabdc1908a1 100644 --- a/Mathlib/Algebra/RingQuot.lean +++ b/Mathlib/Algebra/RingQuot.lean @@ -155,7 +155,7 @@ namespace RingQuot variable (r : R → R → Prop) --- can't be irreducible, causes diamonds in ℤ-algebras +-- can't be irreducible, causes diamonds in ℕ-algebras private def natCast (n : ℕ) : RingQuot r := ⟨Quot.mk _ n⟩