Theorem ArchimedeanClass.mk_natCast

Modification history

2025-12-12 18:47
Mathlib/Algebra/Order/Ring/Archimedean.lean
feat(Algebra/Order/Ring/Archimedean): `⊤ ≠ 0` (#32800) …
Modified ArchimedeanClass.mk_natCastView on Github →
2025-09-13 12:46
Mathlib/Algebra/Order/Ring/Archimedean.lean
feat: archimedean classes of rationals (#28187) …
Added ArchimedeanClass.mk_natCastView on Github →