prod_pi_mulSingle — Mathlib

English

For a family of modules M a and x, the product over s yields an indicator depending on a ∈ s.

Русский

Для семейства модулей M и элементов x произведение по s даёт индикатор по принадлежности a к s.

LaTeX

$$$\\prod_{a' \\in s} \\Pi.mulSingle(a') (f(a'))(a) = \\begin{cases} f(a) & \\text{если } a \\in s \\\\ 1 & \\text{иначе} \\end{cases}.$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_pi_mulSingle {M : ι → Type*} [DecidableEq ι] [∀ a, CommMonoid (M a)] (a : ι) (f : ∀ a, M a)
    (s : Finset ι) : (∏ a' ∈ s, Pi.mulSingle a' (f a') a) = if a ∈ s then f a else 1 :=
  prod_dite_eq _ _ _

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