Commit 2024-09-09 00:57 0c4fd28f

View on Github →

feat(Analysis/SpecialFunctions/Pow/NNReal): Specialise some lemmas to natural/integers powers (#16248) ... and lemmas about negative real powers From LeanAPAP

Estimated changes

modified theorem ENNReal.coe_rpow_of_ne_zero
modified theorem ENNReal.coe_rpow_of_nonneg
modified theorem ENNReal.toNNReal_rpow
modified theorem NNReal.rpow_add'
added theorem NNReal.rpow_add_one'
added theorem NNReal.rpow_add_one
added theorem NNReal.rpow_eq_zero
modified theorem NNReal.rpow_natCast
modified theorem NNReal.rpow_neg
added theorem NNReal.rpow_one_add'
added theorem NNReal.rpow_one_sub'
modified theorem NNReal.rpow_sub'
added theorem NNReal.rpow_sub_one'
added theorem NNReal.rpow_sub_one