Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-11 13:39 60234d18

View on Github →

chore(algebra/archimedean): add exists_pow_lt_of_lt_1 (#4970)

Estimated changes

Modified src/algebra/archimedean.lean

modified theorem exists_int_pow_near'

modified theorem exists_int_pow_near

added theorem exists_nat_pow_near_of_lt_one

added theorem exists_pow_lt_of_lt_one

Modified src/analysis/specific_limits.lean

added theorem uniformity_basis_dist_pow_of_lt_1