prod_unique_nonempty — Mathlib

English

If the index type is unique and the Finset s is nonempty, then the product over s of f equals f at the unique element (default).

Русский

Если тип индексов уникален и s непусто, то произведение по s f равно значению f на единственном элементе (default).

LaTeX

$$$\\text{If } \\text{Unique } \\iota \\text{ and } s\\text{ is Nonempty, then } \\prod_{x \\in s} f(x) = f(\\text{default}).$$$

Lean4

@[to_additive]
theorem prod_unique_nonempty [Unique ι] (s : Finset ι) (f : ι → M) (h : s.Nonempty) : ∏ x ∈ s, f x = f default := by
  rw [h.eq_singleton_default, Finset.prod_singleton]

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