Mathlib v3 is deprecated. Go to Mathlib v4

Theorem exists_nat_pow_near

Modification history

2020-08-15 06:35
src/algebra/archimedean.lean
fix(algebra/archimedean): switch to a more natural and general condition in exists_nat_pow_near (#3782) …
Modified exists_nat_pow_nearView on Github →
2019-03-27 08:20
src/algebra/archimedean.lean
feat(algebra/archimedean): lemmas about powers of elements (#802)
Added exists_nat_pow_nearView on Github →