Generators

Mathlib.GroupTheory.FreeGroup.IsFreeGroup

URI: https://scilib.ai/kg/mathlib#IsFreeGroup.Generators

English

Generators G denotes the underlying set of generators for a free group G; it is a type.

Русский

Generators G обозначает линейку порождающих для свободной группы G; это тип.

LaTeX

$$Generators(G) is a Type$$

Lean4

/-- A set of generators of a free group, chosen arbitrarily -/
def Generators : Type _ :=
  (IsFreeGroup.nonempty_basis (G := G)).choose

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

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

Разделы

Аффилиация

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