Theorem cfcₙ_real_eq_complex

Modification history

2025-07-04 07:44

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

chore: further whitespace fixes (#26708) …

Modified cfcₙ_real_eq_complex View on Github →

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ₙ_real_eq_complex View on Github →