translate_add

Mathlib.Algebra.Group.Translate

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

English

For a,b ∈ G, translate by a+b equals translate by a of translate by b: τ(a+b) f = τ a (τ b f).

Русский

Перенос по сумме равен переносу по a от переноса по b: τ(a+b) f = τ a (τ b f).

LaTeX

$$$\tau(a+b) f = \tau a (\tau b f)$$$

Lean4

theorem translate_add (a b : G) (f : G → α) : τ (a + b) f = τ a (τ b f) := by ext; simp [sub_sub]

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

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

Разделы

Аффилиация

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