Theorems · Inductive type · group theory

HNNExtension.NormalWord.ReducedWord

(G : Type u_1) → [inst : Group G] → Subgroup G → Subgroup G → Type u_1

A reduced word is a head, which is an element of G, followed by the product list of pairs. There should also be no sequences of the form t^u * g * t^-u, where g is in toSubgroup A B u. This is a less strict condition than required for NormalWord.

Defined in

Mathlib.GroupTheory.HNNExtension

Cited by

13 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

Group