prod_neg_index — Mathlib

English

Negating a DFinsupp and then taking the product is the same as taking the product with negated arguments.

Русский

Отрицание DFinsupp и последующее произведение эквивалентны произведению с отрицанием аргументов.

LaTeX

$$$(-g).prod h = g.prod (\\\\lambda i b . h i (-b))$$$

Lean4

@[to_additive]
theorem prod_neg_index [∀ i, AddGroup (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {g : Π₀ i, β i}
    {h : ∀ i, β i → γ} (h0 : ∀ i, h i 0 = 1) : (-g).prod h = g.prod fun i b => h i (-b) :=
  prod_mapRange_index h0

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