coe_dfinsuppProd — Mathlib

English

For finsupp-indexed sums, subtypeDomain distributes over the sum and equals the sum of subtype-domain results.

Русский

Для сумм с индексами подтипов сумма распределяется аналогично и равна сумме результатов подтипа.

LaTeX

$$$ (s.sum h).subtypeDomain p = s.sum (\\lambda c d. (h c d).subtypeDomain p). $$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_dfinsuppProd [MulOneClass R] [CommMonoid S] (f : Π₀ i, β i) (g : ∀ i, β i → R →* S) :
    ⇑(f.prod g) = f.prod fun a b => ⇑(g a b) :=
  coe_finset_prod _ _

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