Commit 2024-11-16 16:13 7b8edbb9

View on Github →

chore(Algebra.Order.Star.Basic): Protected IsSelfAdjoint.mul_self_nonneg and IsSelfAdjoint.sq_nonneg (#19128) Marking these lemmas as protected.

Estimated changes

Modified Mathlib/Algebra/Order/Star/Basic.lean

deleted theorem IsSelfAdjoint.mul_self_nonneg

deleted theorem IsSelfAdjoint.sq_nonneg

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

added theorem IsSelfAdjoint.sq_spectrumRestricts