Theorems · Inductive type · group theory

HNNExtension.NormalWord

{G : Type u_1} → [inst : Group G] → {A B : Subgroup G} → HNNExtension.NormalWord.TransversalPair G A B → Type u_1

Given a TransversalPair, we can make a normal form for words in the HNNExtension G A B φ. The normal form is a head, which is an element of G, followed by the product list of pairs, t ^ u * g, where u is 1 or -1 and g is the chosen element of its right coset of toSubgroup A B u. There should also be no sequences of the form t^u * g * t^-u where g ∈ toSubgroup A B u

Defined in

Mathlib.GroupTheory.HNNExtension

Cited by

36 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

Group