feat(LinearAlgebra/Eigenspace/Matrix): a scalar is in the spectrum iff it's an eigenvalue

Mathlib/LinearAlgebra/Eigenspace/Basic.lean

@@ -506,6 +506,14 @@ theorem hasEigenvalue_iff_mem_spectrum [FiniteDimensional K V] {f : End K V} {μ
 
 alias ⟨_, HasEigenvalue.of_mem_spectrum⟩ := hasEigenvalue_iff_mem_spectrum
 
+theorem mem_spectrum_of_map_eq_smul {f : End R M} {v : M} {a : R} (h0 : v ≠ 0) (h : f v = a • v) :
+    a ∈ spectrum R f :=
+  hasEigenvalue_of_hasEigenvector ⟨by simp [h], h0⟩ |>.mem_spectrum
+
+theorem hasEigenvalue_iff_exists_map_eq_smul {f : End R M} {a : R} :
+    f.HasEigenvalue a ↔ ∃ v ≠ 0, f v = a • v := by
+  simp [hasEigenvalue_iff, Submodule.ne_bot_iff, and_comm]
+
 theorem eigenspace_div (f : End K V) (a b : K) (hb : b ≠ 0) :
     eigenspace f (a / b) = LinearMap.ker (b • f - algebraMap K (End K V) a) :=
   genEigenspace_div f a b hb

Mathlib/LinearAlgebra/Eigenspace/Matrix.lean

@@ -136,6 +136,20 @@ theorem spectrum_toLin (A : Matrix n n R) (b : Basis n R M) :
 theorem spectrum_toLin' (A : Matrix n n R) : spectrum R A.toLin' = spectrum R A :=
   AlgEquiv.spectrum_eq Matrix.toLinAlgEquiv' A
 
+theorem mem_spectrum_of_mulVec_eq_smul {A : Matrix n n R} {v : n → R} {a : R} (h0 : v ≠ 0)
+    (h : A *ᵥ v = a • v) : a ∈ spectrum R A := by
+  rw [← spectrum_toLin']
+  exact mem_spectrum_of_map_eq_smul h0 h
+
+theorem mem_spectrum_iff_exists_mulVec_eq_smul {K : Type*} [Field K] {A : Matrix n n K} {a : K} :
+    a ∈ spectrum K A ↔ ∃ v ≠ 0, A *ᵥ v = a • v := by
+  simp_rw [← spectrum_toLin', ← hasEigenvalue_iff_mem_spectrum,
+    hasEigenvalue_iff_exists_map_eq_smul, toLin'_apply]
+
+theorem isUnit_iff_forall_mulVec_eq_zero {K : Type*} [Field K] {A : Matrix n n K} :
+    IsUnit A ↔ ∀ v, A *ᵥ v = 0 → v = 0 := by
+  simp_rw [← isUnit_toLin'_iff, A.toLin'.isUnit_iff_ker_eq_bot, A.toLin'.ker_eq_bot', toLin'_apply]
+
 end Matrix
 
 /-- The spectrum of the diagonal operator is the range of the diagonal viewed as a function. -/