Theorem cfcₙHomSuperset_id'

Modification history

2025-09-18 15:32
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
refactor: switch to using `Fact (0 ∈ s)` for `ContinuousMapZero.id` (#29563) …
Deleted cfcₙHomSuperset_id'View on Github →
2024-10-26 18:11
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
feat: define `cfcHomSuperset` (#18126) …
Added cfcₙHomSuperset_id'View on Github →