Theorem cfcₙHomSuperset_id

Modification history

2024-10-26 18:11
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
feat: define `cfcHomSuperset` (#18126) …
Added cfcₙHomSuperset_idView on Github →