sub_of_mul_eq_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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