From a940e74ae23aa4cc7704c42e0ff69c39dd108a0a Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Wed, 19 Aug 2026 12:06:24 +1000 Subject: [PATCH 1/2] fix lemma --- Mathlib/Analysis/InnerProductSpace/Spectrum.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Spectrum.lean b/Mathlib/Analysis/InnerProductSpace/Spectrum.lean index b6eaae80d2bd5e..1107d10657dbd2 100644 --- a/Mathlib/Analysis/InnerProductSpace/Spectrum.lean +++ b/Mathlib/Analysis/InnerProductSpace/Spectrum.lean @@ -416,13 +416,13 @@ theorem eigenvalue_nonneg_of_nonneg {μ : ℝ} {T : E →ₗ[𝕜] E} (hμ : Has exact (mul_nonneg_iff_of_pos_right hpos).mp (this ▸ hnn v) theorem eigenvalue_pos_of_pos {μ : ℝ} {T : E →ₗ[𝕜] E} (hμ : HasEigenvalue T μ) - (hnn : ∀ x : E, 0 < RCLike.re ⟪x, T x⟫) : 0 < μ := by + (hnn : ∀ x : E, x ≠ 0 → 0 < RCLike.re ⟪x, T x⟫) : 0 < μ := by obtain ⟨v, hv₁, hv₂⟩ := hμ.exists_hasEigenvector have hpos : (0 : ℝ) < ‖v‖ ^ 2 := by simpa only [sq_pos_iff, norm_ne_zero_iff] using hv₂ simp only [mem_genEigenspace_one] at hv₁ have : RCLike.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2 := mod_cast congr_arg RCLike.re (inner_product_apply_eigenvector hv₁) - exact (mul_pos_iff_of_pos_right hpos).mp (this ▸ hnn v) + exact (mul_pos_iff_of_pos_right hpos).mp (this ▸ hnn v hv₂) end Nonneg From f24777c72c7c0b3fb85d432983cb3d10cb0cfced Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Wed, 19 Aug 2026 12:26:21 +1000 Subject: [PATCH 2/2] unnecessary type annotations --- Mathlib/Analysis/InnerProductSpace/Spectrum.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Spectrum.lean b/Mathlib/Analysis/InnerProductSpace/Spectrum.lean index 1107d10657dbd2..73c9da2afd489b 100644 --- a/Mathlib/Analysis/InnerProductSpace/Spectrum.lean +++ b/Mathlib/Analysis/InnerProductSpace/Spectrum.lean @@ -407,18 +407,18 @@ theorem inner_product_apply_eigenvector {μ : 𝕜} {v : E} {T : E →ₗ[𝕜] simp only [h, inner_smul_right, inner_self_eq_norm_sq_to_K] theorem eigenvalue_nonneg_of_nonneg {μ : ℝ} {T : E →ₗ[𝕜] E} (hμ : HasEigenvalue T μ) - (hnn : ∀ x : E, 0 ≤ RCLike.re ⟪x, T x⟫) : 0 ≤ μ := by + (hnn : ∀ x, 0 ≤ RCLike.re ⟪x, T x⟫) : 0 ≤ μ := by obtain ⟨v, hv₁, hv₂⟩ := hμ.exists_hasEigenvector - have hpos : (0 : ℝ) < ‖v‖ ^ 2 := by simpa only [sq_pos_iff, norm_ne_zero_iff] using hv₂ + have hpos : 0 < ‖v‖ ^ 2 := by simpa only [sq_pos_iff, norm_ne_zero_iff] using hv₂ simp only [mem_genEigenspace_one] at hv₁ have : RCLike.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2 := mod_cast congr_arg RCLike.re (inner_product_apply_eigenvector hv₁) exact (mul_nonneg_iff_of_pos_right hpos).mp (this ▸ hnn v) theorem eigenvalue_pos_of_pos {μ : ℝ} {T : E →ₗ[𝕜] E} (hμ : HasEigenvalue T μ) - (hnn : ∀ x : E, x ≠ 0 → 0 < RCLike.re ⟪x, T x⟫) : 0 < μ := by + (hnn : ∀ x, x ≠ 0 → 0 < RCLike.re ⟪x, T x⟫) : 0 < μ := by obtain ⟨v, hv₁, hv₂⟩ := hμ.exists_hasEigenvector - have hpos : (0 : ℝ) < ‖v‖ ^ 2 := by simpa only [sq_pos_iff, norm_ne_zero_iff] using hv₂ + have hpos : 0 < ‖v‖ ^ 2 := by simpa only [sq_pos_iff, norm_ne_zero_iff] using hv₂ simp only [mem_genEigenspace_one] at hv₁ have : RCLike.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2 := mod_cast congr_arg RCLike.re (inner_product_apply_eigenvector hv₁)