map_finprod — Mathlib

English

Let g be a multiplicative equivalence g : M ≃* N. Then for any f : α → M, g preserves finprod: g(∏ᶠ i, f(i)) = ∏ᶠ i, g(f(i)).

Русский

Пусть g — мультипликативное эквивалентное отображение M к N. Тогда для любого f: α → M сохраняется финпроизводство: g(∏ᶠ i, f(i)) = ∏ᶠ i, g(f(i)).

LaTeX

$$$$ g\left(\prod^{\mathrm{fin}}_{i} f(i)\right) = \prod^{\mathrm{fin}}_{i} g\bigl(f(i)\bigr). $$$$

Lean4

@[to_additive]
theorem map_finprod (g : M ≃* N) (f : α → M) : g (∏ᶠ i, f i) = ∏ᶠ i, g (f i) :=
  g.toMonoidHom.map_finprod_of_injective (EquivLike.injective g) f

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