noncomputable def Matrix.IsHermitian.maxEigenvalue {𝕜 : Type u_1} [Field 𝕜] [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : ℝ

Equations

• hA.maxEigenvalue = iSup hA.eigenvalues