prod_empty' — Mathlib

English

A variant stating that Finset.prod on the empty Finset equals the constant function returning 1: Finset.prod (∅) = (λ _ => 1).

Русский

Вариант: произведение по пустому Finset равно функции, возвращающей 1: Finset.prod (∅) = (λ _, 1).

LaTeX

$$$$ \\mathrm{Finset.prod}(\\emptyset) = \\lambda _ \\mapsto 1. $$$$

Lean4

/-- Variant of `prod_empty` not applied to a function. -/
@[to_additive (attr := grind =)]
theorem prod_empty' : Finset.prod (∅ : Finset ι) = fun (_ : ι → M) => 1 :=
  rfl

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