Update Mathlib/Algebra/RingQuot.lean

leanprover-community · Jul 24, 2023 · b0e9a79 · b0e9a79
1 parent 5dd4831
commit b0e9a79
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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⟩