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
p : Submodule R M
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
μ : R
hμp : Disjoint (eigenspace f μ) p
⊢ eigenspace (LinearMap.restrict f hfp) μ ≤ ⊥
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
p : Submodule R M
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
μ : R
hμp : Disjoint (eigenspace f μ) p
⊢ eigenspace (LinearMap.restrict f hfp) μ = ⊥
rw [eq_bot_iff]
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
p : Submodule R M
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
μ : R
hμp : Disjoint (eigenspace f μ) p
x : { x // x ∈ p }
hx : x ∈ eigenspace (LinearMap.restrict f hfp) μ
⊢ x ∈ ⊥
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
p : Submodule R M
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
μ : R
hμp : Disjoint (eigenspace f μ) p
⊢ eigenspace (LinearMap.restrict f hfp) μ ≤ ⊥
intro x hx
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
p : Submodule R M
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
μ : R
hμp : Disjoint (eigenspace f μ) p
x : { x // x ∈ p }
hx : x ∈ eigenspace (LinearMap.restrict f hfp) μ
⊢ x ∈ ⊥
simpa using hμp.le_bot ⟨eigenspace_restrict_le_eigenspace f hfp μ ⟨x, hx, rfl⟩, x.prop⟩