Theorem inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux

Modification history

2026-02-23 18:16
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
refactor: weaken `IsClosedEmbedding` requirement in `ContinuousFunctionalCalculus` (#35551) …
Added inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAuxView on Github →