Commit 2024-07-09 02:00 7277dced

View on Github →

feat : define ContinuousFunctionalCalculus Instance for Hermitian Matrices over an RCLike Field (#13697) This file contains the requisite lemmas needed to define a ContinuousFunctionalCalculus for Hermitian Matrices over an RCLike Field.

depends on: #13729
depends on: #13765
depends on : #13837
depends on : #13838 Co-Authored by @j-loreaux

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/HermitianFunctionalCalculus.lean

added theorem Matrix.IsHermitian.cfcAux_id

added theorem Matrix.IsHermitian.cfc_eq

added theorem Matrix.IsHermitian.closedEmbedding_cfcAux

added theorem Matrix.IsHermitian.eigenvalues_eq_spectrum_real

added theorem Matrix.finite_real_spectrum