Theorem cfcₙHom_real_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_real_eq_restrictView on Github →