Theorem cfcHomSuperset_id

Modification history

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