Theorem CFC.norm_sqrt

Modification history

2025-05-08 15:46

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Isometric.lean

chore(*): use notation for `Real.sqrt` (#24684) …

Modified CFC.norm_sqrt View on Github →

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