sub_iff_mul_eq_right — Mathlib

English

For star projections p,q in a ring with torsion-free additive structure, q p is a star projection iff q p = p.

Русский

Для звездных проекций p,q в кольце с торовой свободной аддитивной структурой, q p звёздная проекция тогда и только тогда, когда q p = p.

LaTeX

$$IsStarProjection(q - p) \iff q p = p$$

Lean4

/-- `q - p` is a star projection iff `q * p = p`. -/
theorem sub_iff_mul_eq_right [NonUnitalRing R] [StarRing R] [IsAddTorsionFree R] {p q : R} (hp : IsStarProjection p)
    (hq : IsStarProjection q) : IsStarProjection (q - p) ↔ q * p = p :=
  by
  rw [← star_inj]
  simp [star_mul, hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq, sub_iff_mul_eq_left hp hq]

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