prod_cons — Mathlib

English

For DecidableEq ι, prod_insert states that if a ∉ s then ∏ x ∈ insert a s, f x = f a * ∏ x ∈ s, f x.

Русский

При разрешённом равенстве ι, если a не в s, то произведение по insert a s равно f 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_cons (h : a ∉ s) : ∏ x ∈ cons a s h, f x = f a * ∏ x ∈ s, f x :=
  fold_cons h

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