prod_insert — Mathlib

English

Variant of prod_insert for DecidableEq ι with the simple equality: prod_insert' states ∏ x ∈ insert a s, f x = f a * ∏ x ∈ s, f x when a ∉ s.

Русский

Вариант prod_insert для DecidableEq, где a не принадлежит s.

LaTeX

$$$\prod x \in insert a s, f x = f a * \prod x \in s, f x.$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_insert [DecidableEq ι] : a ∉ s → ∏ x ∈ insert a s, f x = f a * ∏ x ∈ s, f x :=
  fold_insert

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