prod_univ_zero — Mathlib

English

Let M be a commutative monoid and f be a function from the empty finite type Fin 0 to M. The product of f over all indices is the identity element of M, i.e. the empty product is 1.

Русский

Пусть M — коммутативный моноид, а f: Fin 0 → M. Произведение по всем элементам диапазона равняется тождественному элементу, то есть пустое произведение равно 1.

LaTeX

$$$\displaystyle \prod_{i \in \varnothing} f(i) = 1$$$

Lean4

/-- A product of a function `f : Fin 0 → M` is `1` because `Fin 0` is empty -/
@[to_additive /-- A sum of a function `f : Fin 0 → M` is `0` because `Fin 0` is empty -/
    ]
theorem prod_univ_zero (f : Fin 0 → M) : ∏ i, f i = 1 :=
  rfl

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