lift_mk

Mathlib.GroupTheory.FreeGroup.Basic

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

English

FreeGroup α is endowed with a group structure (duplicate entry for clarity).

Русский

FreeGroup α повторно образована в виде группы (повторная формулировка).

LaTeX

$$$\\text{Group}(FreeGroup(\\alpha))$ with the usual operations.$$

Lean4

@[to_additive (attr := simp)]
theorem lift_mk : lift f (mk L) = List.prod (L.map fun x => cond x.2 (f x.1) (f x.1)⁻¹) :=
  rfl

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

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

Разделы

Аффилиация

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