Commit 2024-11-04 23:57 bb0335e7

View on Github →

feat(AtTopBot/Archimedean): weaken TC assumptions (#18445) ... from linear ordered archimedean ring to an ordered archimedean ring.

Estimated changes

Modified Mathlib/Algebra/Order/Archimedean/Basic.lean

added theorem exists_int_ge

added theorem exists_int_le

Modified Mathlib/Order/Filter/AtTopBot/Archimedean.lean

modified theorem atBot_hasCountableBasis_of_archimedean

modified theorem atTop_hasCountableBasis_of_archimedean