sub — Mathlib

English

If a and b are idempotent and a b = a and b a = a, then b − a is idempotent.

Русский

Если a и b идемпотентны, и a b = a, b a = a, тогда b − a идемпотентно.

LaTeX

$$IsIdempotentElem (b - a)$$

Lean4

/-- `b - a` is idempotent when `a * b = a` and `b * a = a`. -/
theorem sub [NonUnitalNonAssocRing R] {a b : R} (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) (hab : a * b = a)
    (hba : b * a = a) : IsIdempotentElem (b - a) := by
  simp_rw [IsIdempotentElem, sub_mul, mul_sub, hab, hba, ha.eq, hb.eq, sub_self, sub_zero]

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