sub_of_mul_eq_right — Mathlib

English

If p and q are star projections and q p = p, then q − p is a star projection.

Русский

Если p и q — звездные проекции и q p = p, то q − p — звездная проекция.

LaTeX

$$q p = p ⇒ IsStarProjection(q - p)$$

Lean4

/-- `q - p` is a star projection when `q * p = p`. -/
theorem sub_of_mul_eq_right [NonUnitalNonAssocRing R] [StarRing R] (hp : IsStarProjection p) (hq : IsStarProjection q)
    (hqp : q * p = p) : IsStarProjection (q - p) :=
  hp.sub_of_mul_eq_left hq (by simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hqp)))

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