isIdempotentElem_iff_mul_one_sub_self

Mathlib.Algebra.Ring.Idempotent

URI: https://scilib.ai/kg/mathlib#isIdempotentElem_iff_mul_one_sub_self

← MathLib Explorer

English

IsIdempotentElem(a) iff a(1 − a) = 0.

Русский

IsIdempotentElem(a) тогда и только тогда, когда a(1 − a) = 0.

LaTeX

$$IsIdempotentElem(a) ↔ (a(1 − a) = 0)$$

Lean4

theorem _root_.isIdempotentElem_iff_mul_one_sub_self : IsIdempotentElem a ↔ a * (1 - a) = 0 := by
  rw [mul_sub, mul_one, sub_eq_zero, eq_comm, IsIdempotentElem]

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

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

Разделы

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

Аффилиация

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