prod_singleton

Mathlib.Algebra.BigOperators.Group.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.prod_singleton

English

The product over a singleton set {a} of a function f equals the value f(a).

Русский

Произведение над единичным множеством {a} функции f равно f(a).

LaTeX

$$$\\prod_{x \\in \\{a\\}} f(x) = f(a)$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_singleton (f : ι → M) (a : ι) : ∏ x ∈ singleton a, f x = f a :=
  Eq.trans fold_singleton <| mul_one _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru