Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-20 21:45 c9f48402

View on Github →

refactor(analysis/special_functions/pow): assume n ≠ 0 instead of 0 < n (#15553)

Estimated changes

modified theorem complex.cpow_nat_inv_pow
modified theorem nnreal.pow_nat_rpow_nat_inv
modified theorem nnreal.rpow_nat_inv_pow_nat
modified theorem real.pow_nat_rpow_nat_inv
modified theorem real.rpow_nat_inv_pow_nat