English
If a ∉ s and (s ∩ mulSupport f) is finite, then ∏_{i∈insert a s} f(i) = f(a) · ∏_{i∈s} f(i).
Русский
Если a ∉ s и (s ∩ mulSupport f) конечно, то произведение по 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
/-- A more general version of `finprod_mem_insert` that requires `s ∩ mulSupport f` rather than `s`
to be finite. -/
@[to_additive /-- A more general version of `finsum_mem_insert` that requires `s ∩ support f` rather
than `s` to be finite. -/
]
theorem finprod_mem_insert' (f : α → M) (h : a ∉ s) (hs : (s ∩ mulSupport f).Finite) :
∏ᶠ i ∈ insert a s, f i = f a * ∏ᶠ i ∈ s, f i :=
by
rw [insert_eq, finprod_mem_union' _ _ hs, finprod_mem_singleton]
· rwa [disjoint_singleton_left]
· exact (finite_singleton a).inter_of_left _
