Commit 2024-08-01 04:08 81a4038d

View on Github →

refactor: remove some dependence on circle in C⋆-algebras (#15343)

Estimated changes

Modified Mathlib/Analysis/CstarAlgebra/ContinuousFunctionalCalculus/Instances.lean

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

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

Modified Mathlib/Analysis/CstarAlgebra/ContinuousFunctionalCalculus/Unitary.lean

added theorem cfc_unitary_iff

deleted theorem mem_unitary_of_spectrum_subset_circle

added theorem mem_unitary_of_spectrum_subset_unitary

deleted theorem spectrum_subset_circle_of_mem_unitary

added theorem spectrum_subset_unitary_of_mem_unitary

deleted theorem unitary_iff_isStarNormal_and_spectrum_subset_circle

added theorem unitary_iff_isStarNormal_and_spectrum_subset_unitary