Commit 2025-04-20 13:51 dc4f49f1

feat(ContinuousFunctionalCalculus): cfc applied to products and pi types (#24013) This PR shows that cfc f ⟨a, b⟩ = ⟨cfc f a, cfc f b⟩ and cfc f (x : ∀ i, A i) = fun i => cfc f (x i) and likewise for the non-unital case. Specialized version for nnrpow, rpow and sqrt are also given.