English
If f(a) = 1, then the same equality as above holds: ∏_{i∈insert a s} f(i) = ∏_{i∈s} f(i).
Русский
Если f(a) = 1, то аналогичное равенство справедливо: ∏_{i∈insert a s} f(i) = ∏_{i∈s} f(i).
LaTeX
$$\prod_{i \in \operatorname{insert}(a,s)} f(i) = \prod_{i \in s} f(i)$$
Lean4
/-- If the multiplicative support of `f` is finite, then for every `x` in the domain of `f`, `f x`
divides `finprod f`. -/
theorem finprod_mem_dvd {f : α → N} (a : α) (hf : (mulSupport f).Finite) : f a ∣ finprod f :=
by
by_cases ha : a ∈ mulSupport f
· rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf (Set.Subset.refl _)]
exact Finset.dvd_prod_of_mem f ((Finite.mem_toFinset hf).mpr ha)
· rw [notMem_mulSupport.mp ha]
exact one_dvd (finprod f)
