Theorems · Theorem · group theory

PresentedGroup.ext

∀ {α : Type u_1} {G : Type u_3} [inst : Group G] {rels : Set (FreeGroup α)} {φ ψ : PresentedGroup rels →* G},
  (∀ (x : α), φ (PresentedGroup.of x) = ψ (PresentedGroup.of x)) → φ = ψ

Defined in

Mathlib.GroupTheory.PresentedGroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

Group