non_zero_eigenvalues_eq_rank_range

Stream: Is there code for X?

[Iván Renison]

Hi, do we have something like this?

import Mathlib.Analysis.InnerProductSpace.Spectrum

variable {𝕜 : Type*} [RCLike 𝕜]
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E]
variable {T : E →ₗ[𝕜] E}
variable {n : ℕ}

lemma LinearMap.IsSymmetric.non_zero_eigenvalues_eq_rank_range (hT : T.IsSymmetric)
    (hn : Module.finrank 𝕜 E = n) :
    Finset.card {i : Fin n | hT.eigenvalues hn i ≠ 0} = Module.finrank 𝕜 (LinearMap.range T) :=
  sorry

It does not need to be with exactly that statement. Actually, probably there is a better way to state it, maybe using the complement.
And if it is not, do you have some suggestions on how to prove it?