isFreeGroup — Mathlib

English

If a group G admits a free group basis b, then G is a free group (i.e., it satisfies the universal property of a free group).

Русский

Если группа G имеет базис свободной группы b, то G является свободной группой (то есть удовлетворяет универсальному свойству свободной группы).

LaTeX

$$IsFreeGroup(G)$$

Lean4

/-- A group admitting a free group basis is a free group. -/
theorem isFreeGroup (b : FreeGroupBasis ι G) : IsFreeGroup G :=
  ⟨range b, ⟨b.reindex (Equiv.ofInjective (↑b) b.injective)⟩⟩

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