commute_of_anticommute — Mathlib

English

If an idempotent element a anticommutes with b, then a and b actually commute when one of them is idempotent.

Русский

Если идемпотентный элемент a антикоммутирует с b, то при наличии идемпотентности одного из элементов они commute.

LaTeX

$$Commute a b$$

Lean4

/-- If idempotent `a` and element `b` anti-commute, then they commute.
So anti-commutativity implies commutativity when one of them is idempotent. -/
theorem commute_of_anticommute {a b : R} [NonUnitalSemiring R] [IsAddTorsionFree R] (ha : IsIdempotentElem a)
    (hab : a * b + b * a = 0) : Commute a b :=
  by
  have := mul_eq_zero_of_anticommute ha hab
  rw [this, zero_add] at hab
  rw [Commute, SemiconjBy, hab, this]

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