prod_single_index — Mathlib

English

For a fixed index i and value b, (single i b).prod h = h i b, provided h i 0 = 1.

Русский

Для фиксированного индекса i и значения b, (single i b).prod h = h i b при условии h i 0 = 1.

LaTeX

$$$\\big(\\\\text{single}(i,b)\\\\big).prod h = h i b$$$

Lean4

@[to_additive]
theorem prod_single_index [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {i : ι} {b : β i}
    {h : ∀ i, β i → γ} (h_zero : h i 0 = 1) : (single i b).prod h = h i b :=
  by
  by_cases h : b ≠ 0
  · simp [DFinsupp.prod, support_single_ne_zero h]
  · rw [not_not] at h
    simp [h, h_zero]
    rfl

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