prod_extend_by_one — Mathlib

English

Let s be a finite set and f a function. Then the product over s of (if i ∈ s then f i else 1) equals the product over s of f i, i.e., extending by the indicator preserves the product.

Русский

Пусть s — конечное множество, a функция f. Тогда произведение по s от (if i ∈ s then f i else 1) равно произведению по s от f i; добавление индикатора не меняет произведение.

LaTeX

$$$\displaystyle \prod i \in s, (\text{ite } (i \in s)\ f\ i\ 1) = \prod i \in s, f\ i$$$

Lean4

@[to_additive]
theorem prod_extend_by_one [DecidableEq ι] (s : Finset ι) (f : ι → M) :
    ∏ i ∈ s, (if i ∈ s then f i else 1) = ∏ i ∈ s, f i :=
  (prod_congr rfl) fun _i hi => if_pos hi

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