prod_empty

Mathlib.Algebra.BigOperators.Group.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Fintype.prod_empty

English

If ι is an empty type, then the product over all elements of ι is equal to the identity: ∏_{x:ι} f(x) = 1.

Русский

Если ι пуст, то произведение по всем элементам ι равно единице: ∏ f(x) = 1.

LaTeX

$$$$\prod_{x:\iota} f(x) = 1.$$$$

Lean4

@[to_additive]
theorem prod_empty [IsEmpty ι] (f : ι → M) : ∏ x : ι, f x = 1 :=
  prod_of_isEmpty _

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

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

Разделы

Аффилиация

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