From 7b8edbb98887af54a4cb8e8f76fa279960233c22 Mon Sep 17 00:00:00 2001 From: JonBannon Date: Sat, 16 Nov 2024 16:13:10 +0000 Subject: [PATCH] chore(Algebra.Order.Star.Basic): Protected `IsSelfAdjoint.mul_self_nonneg` and `IsSelfAdjoint.sq_nonneg` (#19128) Marking these lemmas as `protected`. --- Mathlib/Algebra/Order/Star/Basic.lean | 4 ++-- .../CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Order/Star/Basic.lean b/Mathlib/Algebra/Order/Star/Basic.lean index 0297489633917..71d84e9eeb151 100644 --- 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 index b50bedc7fc13c..76c6e66606ed2 100644 --- 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