Theorems · Theorem · group theory

HNNExtension.hom_ext

∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} {M : Type u_3} [inst_1 : Monoid M]
  {f g : HNNExtension G A B φ →* M},
  f.comp HNNExtension.of = g.comp HNNExtension.of → f HNNExtension.t = g HNNExtension.t → f = g

Defined in

Mathlib.GroupTheory.HNNExtension

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupMonoid