Theorem IsStarProjection.mul_right_and_mul_left_of_nonneg_of_le

Modification history

2026-03-10 23:22
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
feat(Analysis/CStarAlgebra/CFC/Order): conjugating with a star projection in a C*-algebra (#35997) …
Added IsStarProjection.mul_right_and_mul_left_of_nonneg_of_leView on Github →