Theorems · Definition · group theory

HNNExtension.NormalWord.ReducedWord.head

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

Every ReducedWord is the product of an element of the group and a word made up of letters each of which is in the transversal. head is that element of the base group.

Defined in

Mathlib.GroupTheory.HNNExtension

Cited by

25 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

Group