English
For star projections p,q in a ring with torsion-free additive structure, q − p is a star projection iff p q = p.
Русский
Для звездных проекций p,q в кольце с торовой свободной аддитивной структурой, q − p звёздная проекция тогда и только тогда, когда p q = p.
LaTeX
$$IsStarProjection(q - p) \iff p q = p$$
Lean4
/-- `q - p` is a star projection iff `p * q = p`. -/
theorem sub_iff_mul_eq_left [NonUnitalRing R] [StarRing R] [IsAddTorsionFree R] {p q : R} (hp : IsStarProjection p)
(hq : IsStarProjection q) : IsStarProjection (q - p) ↔ p * q = p :=
by
rw [isStarProjection_iff, hp.isIdempotentElem.sub_iff hq.isIdempotentElem]
simp_rw [hq.isSelfAdjoint.sub hp.isSelfAdjoint, and_true]
nth_rw 3 [← hp.isSelfAdjoint]
nth_rw 2 [← hq.isSelfAdjoint]
rw [← star_mul, star_eq_iff_star_eq, hp.isSelfAdjoint, eq_comm]
simp_rw [and_self]
