finsuppProd_apply — Mathlib

English

Applying the finsupp product to an argument x is the same as taking the product of the pointwise applications g i fi x.

Русский

При применении произведения finsupp к аргументу x получаем произведение по i из f, применяя g i fi к x.

LaTeX

$$$$ (f \\mathrm{prod} g) x = f \\mathrm{prod} (\\\\lambda i fi, g i fi x) $$$$

Lean4

@[to_additive (attr := simp)]
theorem finsuppProd_apply [Zero β] [MulOneClass N] [CommMonoid P] (f : α →₀ β) (g : α → β → N →* P) (x : N) :
    f.prod g x = f.prod fun i fi => g i fi x :=
  MonoidHom.finset_prod_apply _ _ _

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