∀ {n : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n 𝕜}
  (hA : A.IsHermitian),
  ((Unitary.conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary)
      (Matrix.diagonal (RCLike.ofReal ∘ ⇑0 ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩)) =
    0