English
If for all a ∉ s, f(a) = 1, then ∏_{i∈insert a s} f(i) = ∏_{i∈s} f(i).
Русский
Если для всех a ∉ s выполняется f(a) = 1, то произведение по insert a s равно произведению по s.
LaTeX
$$\left( \forall a \notin s, f(a) = 1 \right) \Rightarrow \prod_{i \in \operatorname{insert}(a,s)} f(i) = \prod_{i \in s} f(i)$$
Lean4
/-- If `f a = 1` when `a ∉ s`, 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` when `a ∉ s`, then the sum of `f i` over `i ∈ insert a s` equals the sum
of `f i` over `i ∈ s`. -/
]
theorem finprod_mem_insert_of_eq_one_if_notMem (h : a ∉ s → f a = 1) : ∏ᶠ i ∈ insert a s, f i = ∏ᶠ i ∈ s, f i :=
by
refine finprod_mem_inter_mulSupport_eq' _ _ _ fun x hx => ⟨?_, Or.inr⟩
rintro (rfl | hxs)
exacts [not_imp_comm.1 h hx, hxs]
