ofMulEquiv

Mathlib.GroupTheory.FreeGroup.IsFreeGroup

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

English

A group is free if there is an isomorphism from a free group on its generators.

Русский

Группа свободна, если существует изоморфизм из свободной группы на её генераторах.

LaTeX

$$IsFreeGroup.ofMulEquiv(e)$$

Lean4

theorem ofMulEquiv (e : G ≃* H) : IsFreeGroup H :=
  ((basis G).map e).isFreeGroup

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

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

Разделы

Аффилиация

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