map_finprod_mem — Mathlib

English

Let g: M ≃* N be a multiplicative equivalence between commutative monoids, and f: α → M. For any finite subset s ⊆ α, g(∏_{i ∈ s} f(i)) = ∏_{i ∈ s} g(f(i)).

Русский

Пусть g: M ≃* N — мультипликативное эквивалентное отображение между коммутативными моноидами, и f: α → M. Для любого конечного множества s ⊆ α выполняется g(∏_{i ∈ s} f(i)) = ∏_{i ∈ s} g(f(i)).

LaTeX

$$$\operatorname{Finite}(s) \Rightarrow g\left(\prod_{i \in s} f(i)\right) = \prod_{i \in s} g(f(i)).$$$

Lean4

@[to_additive]
theorem map_finprod_mem (g : M ≃* N) (f : α → M) {s : Set α} (hs : s.Finite) : g (∏ᶠ i ∈ s, f i) = ∏ᶠ i ∈ s, g (f i) :=
  g.toMonoidHom.map_finprod_mem f hs

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