Theorem IsSelfAdjoint.sq_spectrumRestricts
Modification history
2024-11-16 16:13
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
chore(Algebra.Order.Star.Basic): Protected `IsSelfAdjoint.mul_self_nonneg` and `IsSelfAdjoint.sq_nonneg` (#19128) …
Added IsSelfAdjoint.sq_spectrumRestrictsView on Github →