map_prod — Mathlib

English

For monoids M,N and a homomorphism g: M → N, for any f : ι → M and Finset s, g(∏ x ∈ s, f x) = ∏ x ∈ s, g(f x).

Русский

Для моноида M, N и гомоморфизма g: M → N, для любой функции f: ι → M и конечного множества s выполняется: g(∏ x ∈ s, f x) = ∏ x ∈ s, g(f x).

LaTeX

$$$$ g\\left(\\prod_{x \\in s} f(x)\\right) = \\prod_{x \in s} g(f(x)). $$$$

Lean4

@[to_additive (attr := simp)]
theorem map_prod [CommMonoid M] [CommMonoid N] {G : Type*} [FunLike G M N] [MonoidHomClass G M N] (g : G) (f : ι → M)
    (s : Finset ι) : g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x) := by
  simp only [Finset.prod_eq_multiset_prod, map_multiset_prod, Multiset.map_map]; rfl

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