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
k : ℕ
hμ : HasGeneralizedEigenvalue f μ k
contra : eigenspace 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
k : ℕ
hμ : HasGeneralizedEigenvalue f μ k
⊢ HasEigenvalue f μ
intro contra
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
k : ℕ
hμ : HasGeneralizedEigenvalue f μ k
contra : eigenspace f μ = ⊥
⊢ ↑(generalizedEigenspace f μ) k = ⊥
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
k : ℕ
hμ : HasGeneralizedEigenvalue f μ k
contra : eigenspace f μ = ⊥
⊢ False
apply hμ
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
k : ℕ
hμ : HasGeneralizedEigenvalue f μ k
contra : Function.Injective ↑(f - ↑(algebraMap R (End R M)) μ)
⊢ Function.Injective ↑((f - ↑(algebraMap R (End R M)) μ) ^ k)
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
k : ℕ
hμ : HasGeneralizedEigenvalue f μ k
contra : eigenspace f μ = ⊥
⊢ ↑(generalizedEigenspace f μ) k = ⊥
erw [LinearMap.ker_eq_bot] at contra ⊢
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
k : ℕ
hμ : HasGeneralizedEigenvalue f μ k
contra : Function.Injective ↑(f - ↑(algebraMap R (End R M)) μ)
⊢ Function.Injective (↑(f - ↑(algebraMap R (End R M)) μ)^[k])
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
k : ℕ
hμ : HasGeneralizedEigenvalue f μ k
contra : Function.Injective ↑(f - ↑(algebraMap R (End R M)) μ)
⊢ Function.Injective ↑((f - ↑(algebraMap R (End R M)) μ) ^ k)
rw [LinearMap.coe_pow]
no goals
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
k : ℕ
hμ : HasGeneralizedEigenvalue f μ k
contra : Function.Injective ↑(f - ↑(algebraMap R (End R M)) μ)
⊢ Function.Injective (↑(f - ↑(algebraMap R (End R M)) μ)^[k])
exact Function.Injective.iterate contra k