Theorem CFC.rpow_eq_rpow_rpod

Modification history

2025-05-28 16:23

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

feat: `CFC.sqrt a = cfcₙ Real.sqrt a` (#24859) …

Deleted CFC.rpow_eq_rpow_rpod View on Github →

2025-04-20 13:51

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

feat(ContinuousFunctionalCalculus): `cfc` applied to products and pi types (#24013) …

Added CFC.rpow_eq_rpow_rpod View on Github →