Theorems · Definition · group theory

HNNExtension.toSubgroupEquiv

{G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} → ↥A ≃* ↥B → (u : ℤˣ) → ↥(HNNExtension.toSubgroup A B u) ≃* ↥(HNNExtension.toSubgroup A B (-u))

To avoid duplicating code, we define toSubgroup A B u and toSubgroupEquiv u where u : ℤˣ is 1 or -1. toSubgroup A B u is A when u = 1 and B when u = -1, and toSubgroupEquiv is the group isomorphism from toSubgroup A B u to toSubgroup A B (-u). It is defined to be φ when u = 1 and φ⁻¹ when u = -1.

Defined in

Mathlib.GroupTheory.HNNExtension

Cited by

7 results in Mathlib

Foundations

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

Assumes

Group