translate_sum_right — Mathlib

English

For a finite index set s and a function f, translating the sum by a gives the sum of translations: τ a (∑ i∈s f i) = ∑ i∈s τ a (f i).

Русский

Для конечной индексовой множества s и функции f перенос суммы на a даёт сумму переносов: τ a (∑ i∈s f i) = ∑ i∈s τ a (f i).

LaTeX

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

Lean4

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

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