Zulip Chat Archive
Stream: mathlib4
Topic: ofNat and CommRing.toGrindCommRing_ofNat
Eric Wieser (Jun 03 2025 at 09:08):
Is docs#CommRing.toGrindCommRing_ofNat mis-stated? I thought that OfNat.ofNat was only ever supposed to be called on raw numerals.
Eric Wieser (Jun 03 2025 at 09:09):
Is docs#CommRing.toGrindCommRing_ofNat mis-stated? I thought that OfNat.ofNat was only ever supposed to be called on raw numerals.
Last updated: Dec 20 2025 at 21:32 UTC