Theorem cfcₙHom_nnreal_eq_restrict

Modification history

2024-09-07 15:05

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

feat(ContinuousFunctionalCalculus): The restriction of a non-unital CFC is equal to the original one (#16287) …

Added cfcₙHom_nnreal_eq_restrict View on Github →