Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-27 08:20 52fddda2

View on Github →

feat(algebra/archimedean): lemmas about powers of elements (#802)

Estimated changes

added theorem exists_int_pow_near
added theorem exists_nat_pow_near