finprod_mem_insert_one — Mathlib

English

If f(a) = 1, then ∏_{i∈insert a s} f(i) = ∏_{i∈s} f(i).

Русский

Если f(a) = 1, то произведение по insert a s равно произведению по s.

LaTeX

$$\prod_{i \in \operatorname{insert}(a,s)} f(i) = \prod_{i \in s} f(i)$$

Lean4

/-- If `f a = 1`, then the product of `f i` over `i ∈ insert a s` equals the product of `f i` over
`i ∈ s`. -/
@[to_additive /-- If `f a = 0`, then the sum of `f i` over `i ∈ insert a s` equals the sum of `f i`
          over `i ∈ s`. -/
    ]
theorem finprod_mem_insert_one (h : f a = 1) : ∏ᶠ i ∈ insert a s, f i = ∏ᶠ i ∈ s, f i :=
  finprod_mem_insert_of_eq_one_if_notMem fun _ => h

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