Normal syllable lists for free groups

A syllable list [(x₁, e₁), …, (x_k, e_k)] represents the free group element syllableProd s = x₁ ^ e₁ ⋯ x_k ^ e_k; it is IsSyllableNormal when every exponent is nonzero and consecutive generators are distinct. exists_isSyllableNormal writes any free group element as the product of a normal syllable list.

def FreeGroup.syllableProd {X : Type u_1} (s : List (X × ℤ)) : FreeGroup X

The product x₁ ^ e₁ ⋯ x_k ^ e_k of a list of syllables.

@[simp]

theorem FreeGroup.syllableProd_nil {X : Type u_1} : syllableProd [] = 1

The empty syllable list represents the identity.

@[simp]

theorem FreeGroup.syllableProd_cons {X : Type u_1} (a : X × ℤ) (s : List (X × ℤ)) : syllableProd (a :: s) = of a.1 ^ a.2 * syllableProd s

The product of a nonempty syllable list factors at its head.

def FreeGroup.IsSyllableNormal {X : Type u_1} (s : List (X × ℤ)) : Prop

A syllable list is normal when its exponents are nonzero and consecutive generators are distinct.

theorem FreeGroup.isSyllableNormal_iff {X : Type u_1} {s : List (X × ℤ)} : IsSyllableNormal s ↔ (∀ a ∈ s, a.2 ≠ 0) ∧ List.IsChain (fun (a b : X × ℤ) => a.1 ≠ b.1) s

A syllable list is normal iff its exponents are nonzero and consecutive generators are distinct.

theorem FreeGroup.exists_isSyllableNormal {X : Type u_1} (w : FreeGroup X) : ∃ (s : List (X × ℤ)), IsSyllableNormal s ∧ syllableProd s = w

Every element of a free group is the product of a normal syllable list.