Theorem Matrix.IsHermitian.cfcHom_eq_cfcAux

Modification history

2026-02-23 18:16
Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean
refactor: weaken `IsClosedEmbedding` requirement in `ContinuousFunctionalCalculus` (#35551) …
Added Matrix.IsHermitian.cfcHom_eq_cfcAuxView on Github →