Mathlib Changelog
v4
Changelog
About
Github
Theorem
continuous_cfcₙHom_of_cfcHom
Modification history
2026-02-23 18:16
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
refactor: weaken `IsClosedEmbedding` requirement in `ContinuousFunctionalCalculus` (#35551) …
Added
continuous_cfcₙHom_of_cfcHom
View on Github →