prod_one_sub — Mathlib

English

For a family e, the product of (1 − e_i) over all i is zero when the family is complete orthogonal idempotents.

Русский

Для семейства e произведение (1 − e_i) по всем i равно нулю, когда семейство является полным ортогональным Idempotents.

LaTeX

$$$\\prod i, (1 - e_i) = 0$$$

Lean4

theorem prod_one_sub (he : CompleteOrthogonalIdempotents e) : ∏ i, (1 - e i) = 0 := by
  rw [he.1.prod_one_sub, he.complete, sub_self]

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