translate_add'

Mathlib.Algebra.Group.Translate

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

English

Because addition is commutative, τ(a+b) f = τ(b) (τ(a) f).

Русский

Из за коммутативности сложения имеет место τ(a+b) f = τ(b) (τ(a) f).

LaTeX

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

Lean4

/-- See `translate_add` -/
theorem translate_add' (a b : G) (f : G → α) : τ (a + b) f = τ b (τ a f) := by rw [add_comm, translate_add]

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

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

Разделы

Аффилиация

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