prod_dite_eq — Mathlib

English

For a fixed i, the product over j of the dite expression equals f i rfl.

Русский

Для фиксированного i равняется произведение по j от функции dite: ∏ j, (if h : j = i then f j h else 1) = f i rfl.

LaTeX

$$$\\displaystyle \\prod_{j} \\left( \\text{if } h : j = i \\text{ then } f(j,h) \\text{ else } 1 \\right) = f(i,\\mathrm{rfl})$$$

Lean4

/-- See also `Finset.prod_dite_eq`. -/
@[to_additive /-- See also `Finset.sum_dite_eq`. -/
    ]
theorem prod_dite_eq (i : ι) (f : ∀ j, i = j → M) : ∏ j, (if h : i = j then f j h else 1) = f i rfl := by
  rw [Finset.prod_dite_eq, if_pos (mem_univ _)]

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