prod_neg_index — Mathlib

English

For a finite index set and function f, the product over the negated index set equals the product over the original indices with negated arguments: ∏ i∈-s f(i) = ∏ i∈s f(-i).

Русский

Для конечного набора индексов и функции f выполнено: ∏_{i∈-s} f(i) = ∏_{i∈s} f(-i).

LaTeX

$$$\prod_{i \in -s} f(i) = \prod_{i \in s} f(-i)$$$

Lean4

@[to_additive existing, simp]
theorem prod_neg_index [InvolutiveNeg ι] (s : Finset ι) (f : ι → α) : ∏ i ∈ -s, f i = ∏ i ∈ s, f (-i) :=
  prod_image neg_injective.injOn

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