map_finset_prod — Mathlib

English

Let f : F be a finite-type EquivLike structure with MulEquivClass F M N. Then for any g : α → M, f(∏ i ∈ Finset.univ, g i) = ∏ i ∈ Finset.univ, f(g i).

Русский

Пусть F имеет структуру EquivLike с MulEquivClass M N. Тогда для любого g: α → M выполняется f(∏ i ∈ Finset.univ, g i) = ∏ i ∈ Finset.univ, f(g i).

LaTeX

$$$$ f\left(\prod_{i \in \mathrm{Finset.univ}} g(i)\right) = \prod_{i \in \mathrm{Finset.univ}} f(g(i)). $$$$

Lean4

@[to_additive]
theorem map_finset_prod {α F : Type*} [Fintype α] [EquivLike F M N] [MulEquivClass F M N] (f : F) (g : α → M) :
    f (∏ i : α, g i) = ∏ i : α, f (g i) := by simp [← finprod_eq_prod_of_fintype, MulEquivClass.map_finprod]

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