Theorem CFC.nnnorm_sqrt

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.nnnorm_sqrt View on Github →