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_nearView 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_nearView 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_nearView on Github →
2019-03-27 08:20
src/algebra/archimedean.lean
feat(algebra/archimedean): lemmas about powers of elements (#802)
Added exists_int_pow_nearView on Github →