English
If a ∉ s and s is finite, then ∏_{i∈insert a s} f(i) = f(a)·∏_{i∈s} f(i).
Русский
Если a ∉ s и s конечно, то произведение по insert a s равно f(a) умножить на произведение по s.
LaTeX
$$\prod_{i \in \operatorname{insert}(a,s)} f(i) = f(a) \cdot \prod_{i \in s} f(i)$$
Lean4
/-- Given a finite set `s` and an element `a ∉ s`, the product of `f i` over `i ∈ insert a s` equals
`f a` times the product of `f i` over `i ∈ s`. -/
@[to_additive /-- Given a finite set `s` and an element `a ∉ s`, the sum of `f i` over `i ∈ insert a s`
equals `f a` plus the sum of `f i` over `i ∈ s`. -/
]
theorem finprod_mem_insert (f : α → M) (h : a ∉ s) (hs : s.Finite) : ∏ᶠ i ∈ insert a s, f i = f a * ∏ᶠ i ∈ s, f i :=
finprod_mem_insert' f h <| hs.inter_of_left _
