Theorem CStarAlgebra.linear_combination_nonneg

Modification history

2024-11-27 03:15
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
feat: approximate units in C⋆-algebras (#18506) …
Added CStarAlgebra.linear_combination_nonnegView on Github →