Commit 2023-06-11 15:21 5e3467bd

View on Github →

feat: port Analysis.NormedSpace.Star.Spectrum (#4964)

depends on: #4946

Estimated changes

Modified Mathlib.lean

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

added theorem IsSelfAdjoint.mem_spectrum_eq_re

added theorem IsSelfAdjoint.spectralRadius_eq_nnnorm

added theorem IsSelfAdjoint.val_re_map_spectrum

added theorem IsStarNormal.spectralRadius_eq_nnnorm

added theorem StarAlgHom.nnnorm_apply_le

added theorem StarAlgHom.norm_apply_le

added theorem selfAdjoint.mem_spectrum_eq_re

added theorem selfAdjoint.val_re_map_spectrum

added theorem spectrum.subset_circle_of_unitary

added theorem unitary.spectrum_subset_circle