Theorem: Module.End.has_eigenvector_one (CvxLean/Lib/Math/LinearAlgebra/Eigenspace.lean)

State before:
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
x : M
hx : x ≠ 0
⊢ x ∈ eigenspace 1 1
Tactic:
rw [eigenspace_one]
State after:
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
x : M
hx : x ≠ 0
⊢ x ∈ ⊤

State before:
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
x : M
hx : x ≠ 0
⊢ x ∈ ⊤
Tactic:
apply Submodule.mem_top
State after:
no goals