mathlib
60234d18 - chore(algebra/archimedean): add `exists_pow_lt_of_lt_1` (#4970)

Commit

5 years ago

chore(algebra/archimedean): add `exists_pow_lt_of_lt_1` (#4970) Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author

urkud

Parents