English
If p and q are star projections and pq = 0, then p + q is a star projection.
Русский
Если p и q — звездные проекции и pq = 0, то p + q — звездная проекция.
LaTeX
$$IsStarProjection(p) ∧ IsStarProjection(q) ∧ p q = 0 ⇒ IsStarProjection(p + q)$$
Lean4
/-- The sum of star projections is a star projection if their product is `0`. -/
theorem add [NonUnitalNonAssocSemiring R] [StarRing R] (hp : IsStarProjection p) (hq : IsStarProjection q)
(hpq : p * q = 0) : IsStarProjection (p + q)
where
isSelfAdjoint := hp.isSelfAdjoint.add hq.isSelfAdjoint
isIdempotentElem :=
hp.isIdempotentElem.add hq.isIdempotentElem <| by
rw [hpq, zero_add]
simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hpq))
