Mathlib v3 is deprecated. Go to Mathlib v4

Theorem exists_int_pow_near'

Modification history

2021-10-30 20:45
src/algebra/order/archimedean.lean
chore(*): rename int_pow to zpow (#10058) …
Deleted exists_int_pow_near'View on Github →
2020-11-11 13:39
src/algebra/archimedean.lean
chore(algebra/archimedean): add `exists_pow_lt_of_lt_1` (#4970)
Modified exists_int_pow_near'View on Github →
2020-10-27 11:55
src/algebra/archimedean.lean
refactor(*): drop `decidable_linear_order`, switch to Lean 3.22.0 (#4762) …
Modified exists_int_pow_near'View on Github →
2019-11-19 11:07
src/algebra/archimedean.lean
lemmas about powers of elements (#1688) …
Added exists_int_pow_near'View on Github →