Mathlib Changelog
v4
Changelog
About
Github
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