add_sub_mul_of_commute — Mathlib

English

If p and q are star projections that commute, then p + q − pq is a star projection.

Русский

Если p и q — звездные проекции и коммьютируют, то p + q − pq — звездная проекция.

LaTeX

$$Commute(p,q) ⇒ IsStarProjection(p + q - p q)$$

Lean4

theorem add_sub_mul_of_commute [NonUnitalRing R] [StarRing R] (hpq : Commute p q) (hp : IsStarProjection p)
    (hq : IsStarProjection q) : IsStarProjection (p + q - p * q)
    where
  isIdempotentElem := hp.isIdempotentElem.add_sub_mul_of_commute hpq hq.isIdempotentElem
  isSelfAdjoint :=
    .sub (hp.isSelfAdjoint.add hq.isSelfAdjoint) ((IsSelfAdjoint.commute_iff hp.isSelfAdjoint hq.isSelfAdjoint).mp hpq)

Похожие утверждения