Commit 2024-09-08 06:47 12972e5e

View on Github →

feat: star algebra homomorphisms commute with the continuous functional calculus (#16588)

Estimated changes

Modified Mathlib/Algebra/Algebra/Quasispectrum.lean

added theorem NonUnitalAlgHom.quasispectrum_apply_subset'

added theorem NonUnitalAlgHom.quasispectrum_apply_subset

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

added theorem cfcₙHom_continuous

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean

added theorem NonUnitalStarAlgHom.map_cfcₙ

added theorem NonUnitalStarAlgHomClass.map_cfcₙ

added theorem StarAlgHom.map_cfc

added theorem StarAlgHomClass.map_cfc

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

added theorem cfcHom_continuous

Modified Mathlib/Topology/CompactOpen.lean

Modified Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean

added theorem ContinuousMapZero.continuous_comp_left