Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-09 08:13 10914620

View on Github →

feat(analysis/special_functions/pow): inv_rpow, div_rpow (#2999) Also use notation ℝ≥0 and use nnreal.eq instead of rw ← nnreal.coe_eq.

Estimated changes

added theorem real.log_inv
modified theorem ennreal.coe_mul_rpow
modified theorem ennreal.coe_rpow_of_ne_zero
modified theorem ennreal.coe_rpow_of_nonneg
modified theorem filter.tendsto.nnrpow
modified theorem nnreal.coe_rpow
modified theorem nnreal.continuous_at_rpow
added theorem nnreal.div_rpow
added theorem nnreal.inv_rpow
modified theorem nnreal.mul_rpow
modified theorem nnreal.one_le_rpow
modified theorem nnreal.one_lt_rpow
modified theorem nnreal.one_rpow
modified theorem nnreal.pow_nat_rpow_nat_inv
added theorem nnreal.rpow_add'
modified theorem nnreal.rpow_add
modified theorem nnreal.rpow_eq_pow
modified theorem nnreal.rpow_eq_zero_iff
modified theorem nnreal.rpow_le_one
modified theorem nnreal.rpow_le_rpow
modified theorem nnreal.rpow_lt_one
modified theorem nnreal.rpow_lt_rpow
modified theorem nnreal.rpow_mul
modified theorem nnreal.rpow_nat_cast
modified theorem nnreal.rpow_nat_inv_pow_nat
modified theorem nnreal.rpow_neg
modified theorem nnreal.rpow_one
modified theorem nnreal.rpow_zero
modified theorem nnreal.zero_rpow
added theorem real.div_rpow
added theorem real.inv_rpow
modified theorem real.one_le_rpow