Theorems · Definition · group theory

HNNExtension.NormalWord.ReducedWord.toList

{G : Type u_1} → [inst : Group G] → {A B : Subgroup G} → HNNExtension.NormalWord.ReducedWord G A B → List (ℤˣ × G)

The list of pairs (ℤˣ × G), where each pair (u, g) represents the element t^u * g of HNNExtension G A B φ

Defined in

Mathlib.GroupTheory.HNNExtension

Cited by

31 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext

Assumes

Group