Theorems · Theorem · group theory

PresentedGroup.toGroup.unique

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

Defined in

Mathlib.GroupTheory.PresentedGroup

Cited by

0 results in Mathlib

Foundations

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

Assumes

Group