Theorem PositiveLinearMap.norm_apply_le_of_nonneg

Modification history

2025-04-10 16:38
Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean
chore: deprecate semibundled ordered algebraic typeclasses (#20676) …
Modified PositiveLinearMap.norm_apply_le_of_nonnegView on Github →
2025-03-30 03:51
Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean
feat(CStarAlgebra): define positive maps and show their continuity (#23210) …
Added PositiveLinearMap.norm_apply_le_of_nonnegView on Github →