Theorem ArchimedeanClass.eq_zero_or_top_of_archimedean

Modification history

2025-09-13 12:46
Mathlib/Algebra/Order/Ring/Archimedean.lean
feat: archimedean classes of rationals (#28187) …
Added ArchimedeanClass.eq_zero_or_top_of_archimedeanView on Github →