Theorems · Theorem · group theory

PresentedGroup.ext_iff

∀ {α : 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

0 results in Mathlib

Foundations

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

Assumes

Group