isIdempotentElem_iff_one_sub_mul_self

Mathlib.Algebra.Ring.Idempotent

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem _root_.isIdempotentElem_iff_one_sub_mul_self : IsIdempotentElem a ↔ (1 - a) * a = 0 := by
  rw [sub_mul, one_mul, sub_eq_zero, eq_comm, IsIdempotentElem]

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

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

Разделы

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

Аффилиация

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