mul_sum_of_mem

Mathlib.RingTheory.Idempotents

URI: https://scilib.ai/kg/mathlib#OrthogonalIdempotents.mul_sum_of_mem

← MathLib Explorer

English

If i belongs to a finite set s, then e_i times the sum of e_j over j in s equals e_i.

Русский

Если i принадлежит множеству s, тогда e_i умножить на сумму e_j по j в s даёт e_i.

LaTeX

$$e_i * (\sum_{j \in s} e_j) = e_i$$

Lean4

theorem mul_sum_of_mem (he : OrthogonalIdempotents e) {i : I} {s : Finset I} (h : i ∈ s) : e i * ∑ j ∈ s, e j = e i :=
  by classical simp [Finset.mul_sum, he.mul_eq, h]

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

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

Разделы

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

Аффилиация

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