Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-16 22:44 5db1ae4c

View on Github →

feat(analysis/specific_limits): useful specializations of some lemmas (#12069)

Estimated changes

Modified src/algebra/group_power/order.lean

added theorem pow_le_pow_iff

Modified src/analysis/normed/group/basic.lean

added theorem antilipschitz_with.le_mul_norm_sub

Modified src/analysis/specific_limits.lean

added theorem summable_geometric_two_encode

added theorem tendsto_pow_const_mul_const_pow_of_lt_one

added theorem tendsto_self_mul_const_pow_of_abs_lt_one

added theorem tendsto_self_mul_const_pow_of_lt_one