Eigenspaces of diagonalizable maps

Stream: Is there code for X?

[Andrew Yang]

Do we have the description of eigenspaces of a diagonalizable map?
Concretely:

import Mathlib

variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
variable {ι : Type*} [DecidableEq ι] [Fintype ι] (b : Basis ι K V)
variable (μ : ι → K) (f : Module.End K V) (H : ∀ i, f.HasEigenvector (μ i) (b i))

example (l : K) : f.eigenspace l =
    (Finsupp.supported K _ { j | μ j = l }).comap b.repr := sorry