dfinsuppProd_apply — Mathlib

English

Given δ, and g : γ →+ δ, the composition with liftAddHom satisfies g ∘ liftAddHom f = liftAddHom (a ↦ g ∘ (f a)).

Русский

При композиций g с liftAddHom выполняется равенство g ∘ liftAddHom f = liftAddHom (a ↦ g ∘ (f a)).

LaTeX

$$$ g \\circ \\operatorname{liftAddHom} f = \\operatorname{liftAddHom} (\\lambda a. g \\circ (f a)). $$$

Lean4

@[to_additive]
theorem dfinsuppProd_apply [MulOneClass R] [CommMonoid S] (f : Π₀ i, β i) (g : ∀ i, β i → R →* S) (r : R) :
    (f.prod g) r = f.prod fun a b => (g a b) r :=
  finset_prod_apply _ _ _

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