prod_singleton' — Mathlib

English

For a fixed index a, the product over the singleton {a} is the value of the function evaluated at a, i.e., the evaluation map is the same as the singleton product.

Русский

Для фиксированного индекса a произведение по {a} равно значению функции в a.

LaTeX

$$$\\prod_{x \\in \\{a\\}} f(x) = f(a)\\quad \\text{for all } f : \\iota \\to M$$$

Lean4

/-- Variant of `prod_singleton` not applied to a function. -/
@[to_additive (attr := grind =)]
theorem prod_singleton' (a : ι) : Finset.prod (singleton a) = fun (f : ι → M) => f a :=
  by
  funext f
  simp

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