map_one

Mathlib.GroupTheory.FreeGroup.Basic

URI: https://scilib.ai/kg/mathlib#FreeGroup.map_one

English

For any f : α → β, map f 1 = 1 in FreeGroup α.

Русский

Для любого отображения f: α → β, map f 1 = 1 в FreeGroup α.

LaTeX

$$$ map\\ f\\ (1 : FreeGroup α) = 1 $$$

Lean4

@[to_additive (attr := simp)]
theorem map_one (f : α → β) : f <$> (1 : FreeGroup α) = 1 :=
  (map f).map_one

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

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

Разделы

Аффилиация

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