id'

Mathlib.GroupTheory.FreeGroup.Basic

URI: https://scilib.ai/kg/mathlib#FreeGroup.map.id'

English

The map that sends every element z to z (the identity function) acts trivially on any x: map (fun z => z) x = x.

Русский

Отображение, задающее z ↦ z, действует тривиально: map (fun z => z) x = x.

LaTeX

$$$ \\operatorname{map}(\\lambda z.z)\\, x = x $$$

Lean4

@[to_additive (attr := simp)]
theorem id' (x : FreeGroup α) : map (fun z => z) x = x :=
  map.id x

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

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

Разделы

Аффилиация

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