Theorems · Definition · group theory

HNNExtension.lift

{G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      {φ : ↥A ≃* ↥B} →
        {H : Type u_2} →
          [inst_1 : Group H] →
            (f : G →* H) → (x : H) → (∀ (a : ↥A), x * f ↑a = f ↑(φ a) * x) → HNNExtension G A B φ →* H

Define a function HNNExtension G A B φ →* H, by defining it on G and t

Defined in

Mathlib.GroupTheory.HNNExtension

Cited by

5 results in Mathlib

Foundations

Depth 55 from the axioms · uses propext, Quot.sound

Assumes

GroupGroup