Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-12 00:08 89f4786e

View on Github →

feat(analysis/special_functions/pow): norm_num extension for rpow (#11382) Fixes #11374

Estimated changes

added theorem zpow_neg_coe_of_pos
added theorem norm_num.cpow_neg
added theorem norm_num.cpow_pos
added theorem norm_num.ennrpow_neg
added theorem norm_num.ennrpow_pos
added theorem norm_num.nnrpow_neg
added theorem norm_num.nnrpow_pos
added theorem norm_num.rpow_neg
added theorem norm_num.rpow_pos
added theorem norm_num.zpow_neg
added theorem norm_num.zpow_pos