Theorems · Definition · group theory

PresentedGroup.toGroup

{α : Type u_1} →
  {G : Type u_3} →
    [inst : Group G] →
      {f : α → G} → {rels : Set (FreeGroup α)} → (∀ r ∈ rels, (FreeGroup.lift f) r = 1) → PresentedGroup rels →* G

The extension of a map f : α → G that satisfies the given relations to a group homomorphism from PresentedGroup rels → G.

Defined in

Mathlib.GroupTheory.PresentedGroup

Cited by

3 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Group