lift_of_eq_id

Mathlib.GroupTheory.FreeGroup.Basic

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

English

The lift correspondence identifies the identity function with the identity on FreeGroup.

Русский

Соответствие lift идентифицирует тождественную функцию с тождественной на FreeGroup.

LaTeX

$$$lift\\ (of) = Id_{FreeGroup(\\alpha)}$$$

Lean4

@[to_additive]
theorem lift_of_eq_id (α) : lift of = MonoidHom.id (FreeGroup α) :=
  lift.apply_symm_apply (MonoidHom.id _)

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

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

Разделы

Аффилиация

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