isIdempotentElem_idempotent

Mathlib.Algebra.DirectSum.Idempotents

URI: https://scilib.ai/kg/mathlib#DirectSum.isIdempotentElem_idempotent

← MathLib Explorer

English

For each i, e_i is an idempotent element in R: e_i^2 = e_i.

Русский

Для каждого i элемент e_i является идемпотентом: e_i^2 = e_i.

LaTeX

$$$e_i^2 = e_i$$$

Lean4

theorem isIdempotentElem_idempotent (i : I) : IsIdempotentElem (idempotent V i : R) := by
  rw [IsIdempotentElem, ← decompose_eq_mul_idempotent, idempotent, decompose_coe, of_eq_same]

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

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

Разделы

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

Аффилиация

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