prod_neg_index — Mathlib

English

For finsupp with domain α, and g: α → α → β, the product f.prod g equals 0 iff there exists i with i ∈ supp(f) and g i (f i) = 0.

Русский

Для finsupp f: α →₀ M и g: α → α → β, произведение f.prod g равно 0 тогда и только тогда существует i ∈ supp(f), такое что g i (f i) = 0.

LaTeX

$$$$ f.prod g = 0 \\iff \\exists i \\in \\mathrm{supp}(f),\\ g(i, f(i)) = 0 $$$$

Lean4

@[to_additive]
theorem prod_neg_index [SubtractionMonoid G] [CommMonoid M] {g : α →₀ G} {h : α → G → M} (h0 : ∀ a, h a 0 = 1) :
    (-g).prod h = g.prod fun a b => h a (-b) :=
  prod_mapRange_index h0

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