Commit 2025-01-10 08:14 973fc78a

feat(Algebra/Order/Archimedean/Basic): powers between two elements (#20612) This adds two lemmas on linearly ordered semifields: if 0 < c < 1 and a < b * c, then (under suitable conditions on b) there is a power c ^ n (with n a natural number / an integer) strictly between a and b.