Theorem: Module.End.eigenspace_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
⊢ eigenspace 1 1 = ⊤
Tactic:
apply eq_top_iff.2
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
⊢ ⊤ ≤ eigenspace 1 1

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
⊢ ⊤ ≤ eigenspace 1 1
Tactic:
intros x _
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
a✝ : x ∈ ⊤
⊢ x ∈ eigenspace 1 1

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
a✝ : x ∈ ⊤
⊢ x ∈ eigenspace 1 1
Tactic:
simp only [mem_eigenspace_iff, LinearMap.one_apply, one_smul]
State after:
no goals