prod_insert' — Mathlib

English

Variant of prod_insert' with a general context; similar to the previous lemma but expressed in a different style.

Русский

Вариант предыдущего леммы с другим стилем формулировки.

LaTeX

$$$\text{prod_insert'} (h) : \prod x \in insert a s, h x = h a * \prod x \in s, h x.$$$

Lean4

/-- Variant of `prod_insert` not applied to a function. -/
@[to_additive (attr := grind =)]
theorem prod_insert' [DecidableEq ι] (h : a ∉ s) : Finset.prod (insert a s) = fun (f : ι → M) => f a * ∏ x ∈ s, f x :=
  by
  funext f
  rw [Finset.prod_insert h]

Похожие утверждения