Variance eq zero iff is Eigenvector

lemma variance_eq_zero_iff_isEigenvector (T : H →ₗ.[ℂ] H)    (ψ : T.domain) (hψ_norm : ‖(ψ : H)‖ = 1) :    variance T ψ = 0 ↔      T.IsEigenvector ψ (expectedValue T ψ : ℂ) := by  rw [variance_eq_zero_iff]  constructor  · intro h_centered    refine ⟨h_centered, ?_⟩    intro h_zero    have h_zero' : (ψ : H) = 0 := by simpa using h_zero    have h_norm_zero : ‖(ψ : H)‖ = 0 := by simp [h_zero']    have : (0 : ℝ) = 1 := h_norm_zero.symm.trans hψ_norm    norm_num at this  · intro h_eigen    exact h_eigen.1