English
Let s be a finite set of indices and a an index with the property that if a is not in s then f(a) = 1. Then the product of f over insert(a, s) equals the product of f over s.
Русский
Пусть s — конечное множество индексов, а — индекс such that если a не принадлежит s, то f(a) = 1. Тогда произведение f по insert(a, s) равно произведению f по s.
LaTeX
$$$\\left( a \\notin s \\rightarrow f(a) = 1 \\right) \\Rightarrow \\prod_{x \\in \\operatorname{insert}(a,s)} f(x) = \\prod_{x \\in s} f(x)$$$
Lean4
/-- The product of `f` over `insert a s` is the same as
the product over `s`, as long as `a` is in `s` or `f a = 1`. -/
@[to_additive (attr := simp) /-- The sum of `f` over `insert a s` is the same as
the sum over `s`, as long as `a` is in `s` or `f a = 0`. -/
]
theorem prod_insert_of_eq_one_if_notMem [DecidableEq ι] (h : a ∉ s → f a = 1) : ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x :=
by
by_cases hm : a ∈ s
· simp_rw [insert_eq_of_mem hm]
· rw [prod_insert hm, h hm, one_mul]
