Theorems · Theorem · group theory

HNNExtension.ReducedWord.exists_normalWord_prod_eq

∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (d : HNNExtension.NormalWord.TransversalPair G A B)
  (w : HNNExtension.NormalWord.ReducedWord G A B),
  ∃ w',
    HNNExtension.NormalWord.ReducedWord.prod φ w'.toReducedWord = HNNExtension.NormalWord.ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ HNNExtension.toSubgroup A B (-u)

Defined in

Mathlib.GroupTheory.HNNExtension

Cited by

1 results in Mathlib

Foundations

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

Assumes

Group