Theorems · Theorem · group theory

HNNExtension.induction_on

∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} {motive : HNNExtension G A B φ → Prop}
  (x : HNNExtension G A B φ),
  (∀ (g : G), motive (HNNExtension.of g)) →
    motive HNNExtension.t →
      (∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)) →
        (∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹) → motive x

Defined in

Mathlib.GroupTheory.HNNExtension

Cited by

1 results in Mathlib

Foundations

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

Assumes

Group