English
If a function f on a finite set s takes the value 1 at a, then removing a from the product does not change it: ∏ x∈s.erase a, f x = ∏ x∈s, f x whenever f(a) = 1.
Русский
Если значение функции f на элементе a равно 1, то удаление a из произведения не меняет его: ∏ x∈s.erase a, f x = ∏ x∈s, f x при условии f(a) = 1.
LaTeX
$$$\prod_{x \in s \setminus \{a\}} f(x) = \prod_{x \in s} f(x) \quad\text{if } f(a) = 1$$$
Lean4
/-- If a function applied at a point is 1, a product is unchanged by
removing that point, if present, from a `Finset`. -/
@[to_additive /-- If a function applied at a point is 0, a sum is unchanged by
removing that point, if present, from a `Finset`. -/
]
theorem prod_erase [DecidableEq ι] (s : Finset ι) {f : ι → M} {a : ι} (h : f a = 1) :
∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x := by
rw [← sdiff_singleton_eq_erase]
refine prod_subset sdiff_subset fun x hx hnx => ?_
grind
