add_sub_mul

Mathlib.Algebra.Ring.Idempotent

URI: https://scilib.ai/kg/mathlib#IsIdempotentElem.add_sub_mul

← MathLib Explorer

English

If a and b are idempotent in a commutative ring, then a + b − ab is idempotent.

Русский

Если a и b идемпотентны в коммутативном кольце, то a + b − ab идемпотентно.

LaTeX

$$$(a + b - ab)^2 = a + b - ab$.$$

Lean4

theorem add_sub_mul (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) : IsIdempotentElem (a + b - a * b) :=
  add_sub_mul_of_commute (.all ..) hp hq

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru