prod_insert_one — Mathlib

English

If f(a) = 1, then inserting a into a finite set s does not change the product of f over the set.

Русский

Если f(a) = 1, тогда вставка a в конечное множество s не изменяет произведение.

LaTeX

$$$f(a) = 1 \\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 `f a = 1`. -/
@[to_additive /-- The sum of `f` over `insert a s` is the same as
    the sum over `s`, as long as `f a = 0`. -/
    ]
theorem prod_insert_one [DecidableEq ι] (h : f a = 1) : ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x := by simp [h]

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