Commit 2024-07-08 14:11 411ac5c7

View on Github →

refactor(.../ContinuousFunctionalCalculus/Instances): move Unitary to new file (#14475) Addresses a TODO in the code.

Estimated changes

Modified Mathlib.lean

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

deleted theorem mem_unitary_of_spectrum_subset_circle

deleted theorem spectrum_subset_circle_of_mem_unitary

deleted theorem unitary_iff_isStarNormal_and_spectrum_subset_circle

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

added theorem mem_unitary_of_spectrum_subset_circle

added theorem spectrum_subset_circle_of_mem_unitary

added theorem unitary_iff_isStarNormal_and_spectrum_subset_circle