mul_sum_of_notMem

Mathlib.RingTheory.Idempotents

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

← MathLib Explorer

English

If i is not in s, then e_i times the sum of e_j over j in s equals 0.

Русский

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

LaTeX

$$e_i * (\sum_{j \in s} e_j) = 0 \quad\text{if } i \notin s$$

Lean4

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

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

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

Разделы

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

Аффилиация

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