English
In a monoid, for a finite set s and f: s → M and an element a ∈ s, the product over s equals the product over s without a multiplied by f(a): ∏ x∈s, f x = (∏ x∈s.erase a, f x) · f a.
Русский
В моноиде для конечного множества s и функции f: s → M и элемента a ∈ s произведение по s равно произведению по s без a, умноженному на f(a): ∏ x∈s, f x = (∏ x∈s.erase a, f x) · f a.
LaTeX
$$$\left(\prod_{x \in s \setminus \{a\}} f(x)\right) \cdot f(a) = \prod_{x \in s} f(x)$$$
Lean4
/-- A variant of `Finset.mul_prod_erase` with the multiplication swapped. -/
@[to_additive /-- A variant of `Finset.add_sum_erase` with the addition swapped. -/
]
theorem prod_erase_mul [DecidableEq ι] (s : Finset ι) (f : ι → M) {a : ι} (h : a ∈ s) :
(∏ x ∈ s.erase a, f x) * f a = ∏ x ∈ s, f x := by rw [mul_comm, mul_prod_erase s f h]
