From ad4f90556a70a2ea43bc890b4b0682c97aabe3e7 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Wed, 20 May 2026 03:25:43 +0300
Subject: [PATCH] feat(LinearAlgebra/Matrix/Charpoly/Eigs): generalize to
 `CommRing`s

---
 .../LinearAlgebra/Matrix/Charpoly/Eigs.lean   | 29 ++++++++++---------
 1 file changed, 16 insertions(+), 13 deletions(-)

diff --git a/Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean b/Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean
index c9537890c1fd72..4b140e85ddb83d 100644
--- a/Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean
@@ -63,32 +63,35 @@ open scoped Matrix
 
 namespace Matrix
 
-/-- The roots of the characteristic polynomial are in the spectrum of the matrix. -/
-theorem mem_spectrum_of_isRoot_charpoly [Nontrivial R]
-    {r : R} (hr : IsRoot B.charpoly r) : r ∈ spectrum R B := by
-  simp_all [eval_charpoly, spectrum.mem_iff, isUnit_iff_isUnit_det, algebraMap_eq_diagonal,
+theorem mem_spectrum_iff_not_isUnit_eval_charpoly {r : R} :
+    r ∈ spectrum R B ↔ ¬IsUnit (B.charpoly.eval r) := by
+  simp [eval_charpoly, spectrum.mem_iff, isUnit_iff_isUnit_det, algebraMap_eq_diagonal,
     Pi.algebraMap_def]
 
+/-- The roots of the characteristic polynomial are in the spectrum of the matrix. -/
+theorem mem_spectrum_of_isRoot_charpoly [Nontrivial R] {r : R} (hr : IsRoot B.charpoly r) :
+    r ∈ spectrum R B := by
+  simp [mem_spectrum_iff_not_isUnit_eval_charpoly, hr.eq_zero]
+
 /--
 In fields, the roots of the characteristic polynomial are exactly the spectrum of the matrix.
 The weaker direction is true in nontrivial rings (see `Matrix.mem_spectrum_of_isRoot_charpoly`).
 -/
 theorem mem_spectrum_iff_isRoot_charpoly {r : K} : r ∈ spectrum K A ↔ IsRoot A.charpoly r := by
-  simp [eval_charpoly, spectrum.mem_iff, isUnit_iff_isUnit_det, algebraMap_eq_diagonal,
-    Pi.algebraMap_def]
+  simp [mem_spectrum_iff_not_isUnit_eval_charpoly]
 
-theorem det_eq_prod_roots_charpoly_of_splits (hAps : A.charpoly.Splits) :
-    A.det = (Matrix.charpoly A).roots.prod := by
-  rw [det_eq_sign_charpoly_coeff, ← charpoly_natDegree_eq_dim A,
-    hAps.coeff_zero_eq_prod_roots_of_monic A.charpoly_monic, ← mul_assoc,
+theorem det_eq_prod_roots_charpoly_of_splits [IsDomain R] (hAps : B.charpoly.Splits) :
+    B.det = (Matrix.charpoly B).roots.prod := by
+  rw [det_eq_sign_charpoly_coeff, ← charpoly_natDegree_eq_dim B,
+    hAps.coeff_zero_eq_prod_roots_of_monic B.charpoly_monic, ← mul_assoc,
     ← pow_two, pow_right_comm, neg_one_sq, one_pow, one_mul]
 
-theorem trace_eq_sum_roots_charpoly_of_splits (hAps : A.charpoly.Splits) :
-    A.trace = (Matrix.charpoly A).roots.sum := by
+theorem trace_eq_sum_roots_charpoly_of_splits [IsDomain R] (hAps : B.charpoly.Splits) :
+    B.trace = (Matrix.charpoly B).roots.sum := by
   rcases isEmpty_or_nonempty n with h | _
   · simp
   · rw [trace_eq_neg_charpoly_nextCoeff, neg_eq_iff_eq_neg,
-      ← hAps.nextCoeff_eq_neg_sum_roots_of_monic A.charpoly_monic]
+      ← hAps.nextCoeff_eq_neg_sum_roots_of_monic B.charpoly_monic]
 
 variable (A)