prod_cons' — Mathlib

English

Variant of prod_cons with a function inlined: prod_cons' expresses the product over cons as f a * ∏ x ∈ s, f x.

Русский

Вариант prod_cons с функцией: произведение над cons равняется f a умножить на произведение над s.

LaTeX

$$$\prod_{x \in cons a s} f x = f a * \prod_{x \in s} f x.$$$

Lean4

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

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