Theorem IsStarNormal.instNonUnitalContinuousFunctionalCalculus

Modification history

2026-02-23 18:16

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean

refactor: weaken `IsClosedEmbedding` requirement in `ContinuousFunctionalCalculus` (#35551) …

Added IsStarNormal.instNonUnitalContinuousFunctionalCalculus View on Github →