Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-18 14:55 739e831f

View on Github →

feat(analysis/complex/exponential): real powers of nnreals (#2164)

  • feat(analysis/complex/exponential): real powers of nnreals
  • cleanup
  • mean inequalities in nnreal
  • mean inequalities
  • use < instead of >
  • reviewer's comments

Estimated changes

added theorem complex.cpow_eq_pow
added theorem filter.tendsto.nnrpow
added theorem nnreal.coe_rpow
added theorem nnreal.mul_rpow
added theorem nnreal.one_le_rpow
added theorem nnreal.one_lt_rpow
added theorem nnreal.one_rpow
added theorem nnreal.rpow_add
added theorem nnreal.rpow_eq_pow
added theorem nnreal.rpow_le_one
added theorem nnreal.rpow_le_rpow
added theorem nnreal.rpow_lt_one
added theorem nnreal.rpow_lt_rpow
added theorem nnreal.rpow_mul
added theorem nnreal.rpow_nat_cast
added theorem nnreal.rpow_neg
added theorem nnreal.rpow_one
added theorem nnreal.rpow_zero
added theorem nnreal.zero_rpow
added theorem real.rpow_eq_pow