Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-25 18:38 726b7bfd

View on Github →

feat(analysis/specific_limits): a tfae about "f grows exponentially slower than R ^ n" (#5488) Also add supporting lemmas here and there.

Estimated changes

added theorem pow_bit0_nonneg
added theorem pow_bit0_pos
modified theorem pow_two_nonneg
modified theorem pow_two_pos_of_ne_zero
added theorem abs_pow
modified theorem one_add_mul_le_pow
modified theorem one_add_sub_mul_le_pow
added theorem pow_bit1_neg_iff
added theorem pow_bit1_nonneg_iff
added theorem pow_bit1_nonpos_iff
added theorem pow_bit1_pos_iff
added theorem strict_mono_pow_bit1
modified theorem nnreal.coe_pow