add_sub_mul_of_commute — Mathlib

English

If a and b are idempotent and commute, then a + b − ab is idempotent.

Русский

Если a и b идемпотентны и коммутируют, то a + b − ab идемпотентно.

LaTeX

$$$(a + b - ab)^2 = a + b - ab$ (when a^2=a, b^2=b and ab=ba).$$

Lean4

theorem add_sub_mul_of_commute (h : Commute a b) (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) :
    IsIdempotentElem (a + b - a * b) :=
  by
  simp only [IsIdempotentElem, h.eq, mul_sub, mul_add, sub_mul, add_mul, ha.eq, mul_assoc, add_sub_cancel_right, hb.eq,
    hb.mul_self_mul, add_sub_cancel_left, sub_right_inj]
  rw [← h.eq, ha.mul_self_mul, h.eq, hb.mul_self_mul, add_sub_cancel_right]

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