isIdempotentElem_sum — Mathlib

English

The sum of idempotents in an orthogonal family is again idempotent.

Русский

Сумма идемпотентов из ортогональной семьи снова является идемпотентом.

LaTeX

$$IsIdempotentElem\left(\sum_{i \in s} e_i\right)$$

Lean4

theorem isIdempotentElem_sum (he : OrthogonalIdempotents e) {s : Finset I} : IsIdempotentElem (∑ i ∈ s, e i) := by
  classical simp [IsIdempotentElem, Finset.sum_mul, Finset.mul_sum, he.mul_eq]

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