remove isUnit_iff_forall_map_eq_zero

Author: SnirBroshi

Mathlib/LinearAlgebra/Eigenspace/Basic.lean

@@ -514,12 +514,6 @@ 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 isUnit_iff_forall_map_eq_zero [FiniteDimensional K V] {f : End K V} :
-    IsUnit f ↔ ∀ v, f v = 0 → v = 0 := by
-  simp_rw [← spectrum.zero_notMem_iff K, ← hasEigenvalue_iff_mem_spectrum,
-    hasEigenvalue_iff_exists_map_eq_smul, zero_smul]
-  grind only
-
 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

@@ -148,7 +148,7 @@ theorem mem_spectrum_iff_exists_mulVec_eq_smul {K : Type*} [Field K] {A : Matrix
 
 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, isUnit_iff_forall_map_eq_zero, toLin'_apply]
+  simp_rw [← isUnit_toLin'_iff, A.toLin'.isUnit_iff_ker_eq_bot, A.toLin'.ker_eq_bot', toLin'_apply]
 
 end Matrix