Theorem CFC.norm_nnrpow

Modification history

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