Mathlib Changelog
v4
Changelog
About
Github
Theorem
cfcₙHom_mem_elemental
Modification history
2026-03-23 17:30
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Range.lean
feat: generalize results on the range of the continuous functional calculus to avoid closed embeddings (#36908) …
Added
cfcₙHom_mem_elemental
View on Github →