translate_zero

Mathlib.Algebra.Group.Translate

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

English

For a group G and a function f: G → α, translating by 0 leaves f unchanged: τ 0 f = f.

Русский

Для группы G и функции f: G → α перенос на 0 не изменяет f: τ 0 f = f.

LaTeX

$$$\tau 0 f = f$$$

Lean4

@[simp]
theorem translate_zero (f : G → α) : τ 0 f = f := by ext; simp

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

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

Разделы

Аффилиация

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