K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End R M
μ : R
hμ : HasEigenvalue f μ
h_unit : IsUnit (↑(algebraMap R (End R M)) μ - f)
⊢ False
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End R M
μ : R
hμ : HasEigenvalue f μ
⊢ μ ∈ spectrum R f
refine' spectrum.mem_iff.mpr fun h_unit => _
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End R M
μ : R
hμ : HasEigenvalue f μ
h_unit : IsUnit (↑(algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv (IsUnit.unit h_unit)
⊢ False
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End R M
μ : R
hμ : HasEigenvalue f μ
h_unit : IsUnit (↑(algebraMap R (End R M)) μ - f)
⊢ False
set f' := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
case intro
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End R M
μ : R
hμ : HasEigenvalue f μ
h_unit : IsUnit (↑(algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv (IsUnit.unit h_unit)
v : M
hv : HasEigenvector f μ v
⊢ False
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End R M
μ : R
hμ : HasEigenvalue f μ
h_unit : IsUnit (↑(algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv (IsUnit.unit h_unit)
⊢ False
rcases hμ.exists_hasEigenvector with ⟨v, hv⟩
case intro
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End R M
μ : R
hμ : HasEigenvalue f μ
h_unit : IsUnit (↑(algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv (IsUnit.unit h_unit)
v : M
hv : HasEigenvector f μ v
⊢ μ • v - ↑f v = 0
case intro
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End R M
μ : R
hμ : HasEigenvalue f μ
h_unit : IsUnit (↑(algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv (IsUnit.unit h_unit)
v : M
hv : HasEigenvector f μ v
⊢ False
refine' hv.2 ((LinearMap.ker_eq_bot'.mp f'.ker) v (_ : μ • v - f v = 0))
no goals
case intro
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End R M
μ : R
hμ : HasEigenvalue f μ
h_unit : IsUnit (↑(algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv (IsUnit.unit h_unit)
v : M
hv : HasEigenvector f μ v
⊢ μ • v - ↑f v = 0
rw [hv.apply_eq_smul, sub_self]