Commit 2023-06-12 18:27 f16a4091

View on Github →

feat: port Analysis.NormedSpace.Star.ContinuousFunctionalCalculus (#4977)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus.lean

added theorem StarSubalgebra.coe_isUnit

added theorem StarSubalgebra.isUnit_coe_inv_mem

added theorem StarSubalgebra.mem_spectrum_iff

added theorem StarSubalgebra.spectrum_eq

added theorem continuousFunctionalCalculus_map_id

added theorem elementalStarAlgebra.bijective_characterSpaceToSpectrum

added theorem elementalStarAlgebra.continuous_characterSpaceToSpectrum

added theorem elementalStarAlgebra.isUnit_of_isUnit_of_isStarNormal

added theorem spectrum_star_mul_self_of_isStarNormal