map_prod — Mathlib

English

Let g be a RingEquiv R → S; for any finite set s and function f: α → R, g (∏_{x∈s} f x) = ∏_{x∈s} g(f x).

Русский

Пусть g – кольцевой эквивалент R к S; для любого конечного множества s и функции f: α → R выполняется 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

protected theorem map_prod [CommSemiring R] [CommSemiring S] (g : R ≃+* S) (f : α → R) (s : Finset α) :
    g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x) :=
  map_prod g f s

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