translate_translate

Mathlib.Algebra.Group.Translate

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

English

Composition of translations is additive: τ a (τ b f) = τ(a+b) f for a,b ∈ G.

Русский

Сложение переносов даёт сумму: τ a (τ b f) = τ(a+b) f для a,b ∈ G.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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