Theorem ContinuousMapZero.norm_def

Modification history

2024-10-30 16:54
Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean
feat: positive contractions in a Cā‹†-algebra form a directed set (#18016)
Added ContinuousMapZero.norm_defView on Github ā†’