Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-30 10:26 aa944bff

View on Github →

feat(analysis/exponential): real powers, cpow_nat_inv_pow (#647)

Estimated changes

added theorem complex.abs_cpow_real
added theorem complex.cpow_add
added theorem complex.cpow_def
added theorem complex.cpow_int_cast
added theorem complex.cpow_mul
added theorem complex.cpow_nat_cast
added theorem complex.cpow_neg
added theorem complex.cpow_one
added theorem complex.cpow_zero
added theorem complex.of_real_cpow
added theorem complex.one_cpow
deleted theorem complex.pow_add
deleted theorem complex.pow_def
deleted theorem complex.pow_int_cast
deleted theorem complex.pow_mul
deleted theorem complex.pow_nat_cast
added theorem complex.zero_cpow
added theorem real.one_rpow
added theorem real.rpow_add
added theorem real.rpow_def
added theorem real.rpow_int_cast
added theorem real.rpow_mul
added theorem real.rpow_nat_cast
added theorem real.rpow_neg
added theorem real.rpow_one
added theorem real.rpow_zero
added theorem real.zero_rpow