Theorem exists_rat_pow_btwn

Modification history

2025-01-04 14:04
Mathlib/Algebra/Order/Archimedean/Basic.lean
chore: make uniqueness of conditionally complete linearly ordered archimedean fields independent of the construction of `Real` (#20242) …
Added exists_rat_pow_btwnView on Github →