finprod_mem_singleton — Mathlib

English

The product of f over the singleton {a} is f(a): ∏_{i∈{a}} f(i) = f(a).

Русский

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

LaTeX

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

Lean4

/-- The product of `f i` over `i ∈ {a}` equals `f a`. -/
@[to_additive /-- The sum of `f i` over `i ∈ {a}` equals `f a`. -/
    ]
theorem finprod_mem_singleton : (∏ᶠ i ∈ ({ a } : Set α), f i) = f a := by
  rw [← Finset.coe_singleton, finprod_mem_coe_finset, Finset.prod_singleton]

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