map_finprod_plift — Mathlib

English

For a monoid homomorphism f and a function g with finite multiplicative support, the map of the finprod equals the finprod of the mapped values.

Русский

Для гомоморфизма моноидов f и функции g с конечной поддержкой умножения, отображение финпроизводства равно финпроизводству отображённых значений.

LaTeX

$$$f(\\prod^{\\infty}_{x} g(x)) = \\prod^{\\infty}_{x} f(g(x))$$$

Lean4

@[to_additive]
theorem map_finprod_plift (f : M →* N) (g : α → M) (h : (mulSupport <| g ∘ PLift.down).Finite) :
    f (∏ᶠ x, g x) = ∏ᶠ x, f (g x) :=
  by
  rw [finprod_eq_prod_plift_of_mulSupport_subset h.coe_toFinset.ge, finprod_eq_prod_plift_of_mulSupport_subset,
    map_prod]
  rw [h.coe_toFinset]
  exact mulSupport_comp_subset f.map_one (g ∘ PLift.down)

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