case intro.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
p : Submodule R M
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
μ : R
x : { x // x ∈ p }
hx : x ∈ ↑(eigenspace (LinearMap.restrict f hfp) μ)
⊢ ↑(Submodule.subtype p) x ∈ eigenspace f μ
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
⊢ Submodule.map (Submodule.subtype p) (eigenspace (LinearMap.restrict f hfp) μ) ≤ eigenspace f μ
rintro a ⟨x, hx, rfl⟩
case intro.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
p : Submodule R M
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
μ : R
x : { x // x ∈ p }
hx : { val := ↑f ↑x, property := (_ : ↑f ↑x ∈ p) } = μ • x
⊢ ↑f (↑(Submodule.subtype p) x) = μ • ↑(Submodule.subtype p) x
case intro.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
p : Submodule R M
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
μ : R
x : { x // x ∈ p }
hx : x ∈ ↑(eigenspace (LinearMap.restrict f hfp) μ)
⊢ ↑(Submodule.subtype p) x ∈ eigenspace f μ
simp only [SetLike.mem_coe, mem_eigenspace_iff, LinearMap.restrict_apply] at hx ⊢
no goals
case intro.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
p : Submodule R M
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
μ : R
x : { x // x ∈ p }
hx : { val := ↑f ↑x, property := (_ : ↑f ↑x ∈ p) } = μ • x
⊢ ↑f (↑(Submodule.subtype p) x) = μ • ↑(Submodule.subtype p) x
exact congr_arg Subtype.val hx