Theorems · Theorem · group theory

PresentedGroup.to_group_eq_one_of_mem_closure

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

Defined in

Mathlib.GroupTheory.PresentedGroup

Cited by

0 results in Mathlib

Foundations

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

Assumes

Group