chore(Algebra.Order.Star.Basic): Protected `IsSelfAdjoint.mul_self_no…

…nneg` and `IsSelfAdjoint.sq_nonneg` (#19128) Marking these lemmas as `protected`.
leanprover-community · Nov 16, 2024 · 7b8edbb · 7b8edbb
1 parent b4ef117
commit 7b8edbb
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/Mathlib/Algebra/Order/Star/Basic.lean b/Mathlib/Algebra/Order/Star/Basic.lean
@@ -169,7 +169,7 @@ theorem mul_star_self_nonneg (r : R) : 0 ≤ r * star r := by
   simpa only [star_star] using star_mul_self_nonneg (star r)
 
 @[aesop safe apply (rule_sets := [CStarAlgebra])]
-theorem IsSelfAdjoint.mul_self_nonneg {a : R} (ha : IsSelfAdjoint a) : 0 ≤ a * a := by
+protected theorem IsSelfAdjoint.mul_self_nonneg {a : R} (ha : IsSelfAdjoint a) : 0 ≤ a * a := by
   simpa [ha.star_eq] using star_mul_self_nonneg a
 
 @[aesop safe apply]
@@ -302,7 +302,7 @@ lemma star_lt_one_iff {x : R} : star x < 1 ↔ x < 1 := by
   simpa using star_lt_star_iff (x := x) (y := 1)
 
 @[aesop safe apply (rule_sets := [CStarAlgebra])]
-theorem IsSelfAdjoint.sq_nonneg {a : R} (ha : IsSelfAdjoint a) : 0 ≤ a ^ 2 := by
+protected theorem IsSelfAdjoint.sq_nonneg {a : R} (ha : IsSelfAdjoint a) : 0 ≤ a ^ 2 := by
   simp [sq, ha.mul_self_nonneg]
 
 end Semiring

diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
@@ -409,11 +409,11 @@ lemma SpectrumRestricts.nnreal_add {a b : A} (ha₁ : IsSelfAdjoint a)
   gcongr
   all_goals rw [← SpectrumRestricts.nnreal_iff_nnnorm] <;> first | rfl | assumption
 
-protected lemma IsSelfAdjoint.sq_spectrumRestricts {a : A} (ha : IsSelfAdjoint a) :
+lemma IsSelfAdjoint.sq_spectrumRestricts {a : A} (ha : IsSelfAdjoint a) :
     SpectrumRestricts (a ^ 2) ContinuousMap.realToNNReal := by
   rw [SpectrumRestricts.nnreal_iff, ← cfc_id (R := ℝ) a, ← cfc_pow .., cfc_map_spectrum ..]
   rintro - ⟨x, -, rfl⟩
-  exact _root_.sq_nonneg (id x)
+  exact sq_nonneg x
 
 open ComplexStarModule