Commit 2026-03-10 23:22 a41960bd

View on Github →

feat(Analysis/CStarAlgebra/CFC/Order): conjugating with a star projection in a C*-algebra (#35997) When e is a star projection and 0 ≤ a ≤ e, we get e * a * e = a.

Estimated changes

Modified Mathlib/Algebra/Algebra/Unitization.lean

added theorem Unitization.inr_inj

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

added theorem IsStarProjection.conjugate_of_nonneg_of_le

added theorem IsStarProjection.mul_right_and_mul_left_of_nonneg_of_le

added theorem Unitization.sqrt_inr