Commit 2024-04-07 19:21 0a6649f3

View on Github →

feat: generically, the restriction of a continuous functional calculus is equal to the original (#11958)

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Restrict.lean

added theorem SpectrumRestricts.cfcHom_eq_restrict

added theorem SpectrumRestricts.cfc_eq_restrict

added theorem SpectrumRestricts.closedEmbedding_starAlgHom

added theorem SpectrumRestricts.starAlgHom_id

Modified Mathlib/Topology/ContinuousFunction/FunctionalCalculus.lean

added theorem cfcHom_eq_cfc_extend

Modified Mathlib/Topology/ContinuousFunction/NonUnitalFunctionalCalculus.lean

added theorem cfcₙHom_eq_cfcₙ_extend