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
inst✝ : FiniteDimensional K V
f : End K V
k : ℕ
μ : K
hx : HasEigenvalue f μ
hk : 0 < k
⊢ 0 = finrank K { x // x ∈ ⊥ }
rw [finrank_bot]