translate_prod_right — Mathlib

English

Let a ∈ G and f i ∈ G → M with M a CommMonoid. The translate by a distributes over product: τ a (∏ i∈s f i) = ∏ i∈s τ a (f i).

Русский

Пусть a ∈ G, f i ∈ G → M и M коммономод; перенос по a распределяется по произведению: τ a (∏ i∈s f i) = ∏ i∈s τ a (f i).

LaTeX

$$$\tau a\Big(\prod_{i\in s} f(i)\Big) = \prod_{i\in s} \tau a\big(f(i)\big)$$$

Lean4

theorem translate_prod_right (a : G) (f : ι → G → M) (s : Finset ι) : τ a (∏ i ∈ s, f i) = ∏ i ∈ s, τ a (f i) := by ext;
  simp

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