mul_of_commute — Mathlib

English

If a and b are idempotent and commute in a semigroup, then their product a b is idempotent.

Русский

Если элементы a и b идемпотентны и коммутируют в полугруппе, то их произведение a b идемпотентно.

LaTeX

$$$\\text{IsIdempotentElem}(a b).$$$

Lean4

theorem mul_of_commute (hab : Commute a b) (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) :
    IsIdempotentElem (a * b) := by rw [IsIdempotentElem, hab.symm.mul_mul_mul_comm, ha.eq, hb.eq]

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