translate_comm — Mathlib

English

Translations commute: τ a (τ b f) = τ b (τ a f) because addition is commutative on the underlying group.

Русский

Переносы коммутируют: τ a (τ b f) = τ b (τ a f) вследствие коммутативности сложения.

LaTeX

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

Lean4

theorem translate_comm (a b : G) (f : G → α) : τ a (τ b f) = τ b (τ a f) := by
  rw [← translate_add, translate_add']
    -- We make `simp` push the `τ` outside

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