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 m : ℕ
hm : k ≤ m
hk : ↑(generalizedEigenspace f μ) k ≠ ⊥
⊢ ↑(generalizedEigenspace f μ) m ≠ ⊥
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 m : ℕ
hm : k ≤ m
hk : HasGeneralizedEigenvalue f μ k
⊢ HasGeneralizedEigenvalue f μ m
unfold HasGeneralizedEigenvalue at *
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 m : ℕ
hm : k ≤ m
hk : ↑(generalizedEigenspace f μ) m = ⊥
⊢ ↑(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 m : ℕ
hm : k ≤ m
hk : ↑(generalizedEigenspace f μ) k ≠ ⊥
⊢ ↑(generalizedEigenspace f μ) m ≠ ⊥
contrapose! hk
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 m : ℕ
hm : k ≤ m
hk : ↑(generalizedEigenspace f μ) m = ⊥
⊢ ↑(generalizedEigenspace f μ) k ≤ ↑(generalizedEigenspace f μ) m
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 m : ℕ
hm : k ≤ m
hk : ↑(generalizedEigenspace f μ) m = ⊥
⊢ ↑(generalizedEigenspace f μ) k = ⊥
rw [← le_bot_iff, ← hk]
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 m : ℕ
hm : k ≤ m
hk : ↑(generalizedEigenspace f μ) m = ⊥
⊢ ↑(generalizedEigenspace f μ) k ≤ ↑(generalizedEigenspace f μ) m
exact (f.generalizedEigenspace μ).monotone hm