Theorem ArchimedeanClass.mk_eq_zero_of_archimedean

Modification history

2026-01-08 11:26
Mathlib/Algebra/Order/Ring/Archimedean.lean
refactor: make `LinearOrderedCommMonoidWithZero`s cancellative (#31749) …
Modified ArchimedeanClass.mk_eq_zero_of_archimedeanView on Github →
2025-09-13 12:46
Mathlib/Algebra/Order/Ring/Archimedean.lean
feat: archimedean classes of rationals (#28187) …
Added ArchimedeanClass.mk_eq_zero_of_archimedeanView on Github →