Theorem NNReal.monotone_nnrpow_const

Modification history

2025-01-22 02:43
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
feat(ContinuousFunctionalCalculus): `‖sqrt a‖ = sqrt ‖a‖` and `‖a ^ r‖ = ‖a‖^r` for an isometric CFC (#20819) …
Added NNReal.monotone_nnrpow_constView on Github →