prod_one_sub — Mathlib

English

The product over a finite set of (1 − e_i) equals 1 minus the sum of the e_i, when the e_i are pairwise orthogonal idempotents.

Русский

Произведение по i из конечного множества (1 − e_i) равно 1 минус сумма e_i, если e_i ортогональные идемпотенты попарно.

LaTeX

$$$\\prod i \\in s, (1 - e_i) = 1 - \\sum i \\in s, e_i$$$

Lean4

theorem prod_one_sub {I : Type*} {e : I → R} (he : OrthogonalIdempotents e) (s : Finset I) :
    ∏ i ∈ s, (1 - e i) = 1 - ∑ i ∈ s, e i := by
  induction s using Finset.cons_induction with
  | empty => simp
  | cons a s has ih => simp [ih, sub_mul, mul_sub, he.mul_sum_of_notMem has, sub_sub]

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