sum_translate

Mathlib.Algebra.Group.Translate

URI: https://scilib.ai/kg/mathlib#sum_translate

English

For a finite type G, the sum over G of translate a f equals the sum over G of f: ∑ b τ a f b = ∑ b f b.

Русский

Для конечного типа G сумма по всем элементам переходит: ∑ b τ a f b = ∑ b f b.

LaTeX

$$$\sum_{b} \tau a f(b) = \sum_{b} f(b)$$$

Lean4

theorem sum_translate [Fintype G] (a : G) (f : G → M) : ∑ b, τ a f b = ∑ b, f b :=
  Fintype.sum_equiv (Equiv.subRight _) _ _ fun _ ↦ rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru