Theorem exists_int_ge

Modification history

2026-04-11 09:33
Mathlib/Algebra/Order/Archimedean/Basic.lean
chore: move `Archimedean` to a new `Defs` file (#33894) …
Modified exists_int_geView on Github →
2024-11-04 23:57
Mathlib/Algebra/Order/Archimedean/Basic.lean
feat(AtTopBot/Archimedean): weaken TC assumptions (#18445) …
Added exists_int_geView on Github →