Commit 2024-06-23 01:13 8ca31411

View on Github →

feat(ContinuousFunctionalCalculus): add lemmas about the CFC applied to finite sums (#13842)

Estimated changes

Modified Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean

added def ContinuousMapZero.coeFnAddMonoidHom

added theorem ContinuousMapZero.coe_sum

Modified Mathlib/Topology/ContinuousFunction/FunctionalCalculus.lean

added theorem cfc_apply_pi

added theorem cfc_sum

added theorem cfc_sum_univ

Modified Mathlib/Topology/ContinuousFunction/NonUnitalFunctionalCalculus.lean

added theorem cfcₙ_apply_pi

added theorem cfcₙ_sum

added theorem cfcₙ_sum_univ