Theorem CStarAlgebra.exists_sum_four_nonneg

Modification history

2025-03-30 03:51
Mathlib/Analysis/CStarAlgebra/SpecialFunctions/PosPart.lean
feat(CStarAlgebra): define positive maps and show their continuity (#23210) …
Added CStarAlgebra.exists_sum_four_nonnegView on Github →