instIsFreeGroup — Mathlib

English

The free product of free groups is itself a free group.

Русский

Свободное произведение свободных групп снова является свободной группой.

LaTeX

$$$\mathrm{IsFreeGroup}(\mathrm{CoprodI} G)$$$

Lean4

/-- The free product of free groups is itself a free group. -/
instance {ι : Type*} (G : ι → Type*) [∀ i, Group (G i)] [∀ i, IsFreeGroup (G i)] : IsFreeGroup (CoprodI G) :=
  (FreeGroupBasis.coprodI (fun i ↦ IsFreeGroup.basis (G i))).isFreeGroup

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