Theorems · Theorem · group theory

PresentedGroup.toGroup.of

∀ {α : Type u_1} {G : Type u_3} [inst : Group G] {f : α → G} {rels : Set (FreeGroup α)}
  (h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1) {x : α}, (PresentedGroup.toGroup h) (PresentedGroup.of x) = f 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