of_mul_add — Mathlib

English

If a and b are idempotent elements of a semiring, then a^2 = a and b^2 = b.

Русский

Если элементы a и b идемпотентны в полугруппе, то a^2 = a и b^2 = b.

LaTeX

$$$a^2 = a \quad\text{and}\quad b^2 = b.$$$

Lean4

theorem of_mul_add (mul : a * b = 0) (add : a + b = 1) : IsIdempotentElem a ∧ IsIdempotentElem b :=
  by
  simp_rw [IsIdempotentElem]; constructor
  · conv_rhs => rw [← mul_one a, ← add, mul_add, mul, add_zero]
  · conv_rhs => rw [← one_mul b, ← add, add_mul, mul, zero_add]

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