This file defines some extra lemmas for free groups, in particular about cyclically reduced words.

Main declarations

• FreeGroup.IsCyclicallyReduced: the predicate for cyclically reduced words

def FreeGroup.IsCyclicallyReduced {α : Type u} (L : List (α × Bool)) : Prop

Predicate asserting that the word L is cyclically reduced, i.e., it is reduced and furthermore the first and the last letter of the word do not cancel. The empty word is by convention also cyclically reduced.

Equations

• FreeGroup.IsCyclicallyReduced L = (FreeGroup.IsReduced L ∧ ∀ a ∈ L.getLast?, ∀ b ∈ L.head?, a.1 = b.1 → a.2 = b.2)

def FreeAddGroup.IsCyclicallyReduced {α : Type u} (L : List (α × Bool)) : Prop

Predicate asserting that the word L is cyclically reduced, i.e., it is reduced and furthermore the first and the last letter of the word do not cancel. The empty word is by convention also cyclically reduced.

Equations

• FreeAddGroup.IsCyclicallyReduced L = (FreeAddGroup.IsReduced L ∧ ∀ a ∈ L.getLast?, ∀ b ∈ L.head?, a.1 = b.1 → a.2 = b.2)

theorem FreeGroup.isCyclicallyReduced_iff {α : Type u} {L : List (α × Bool)} : IsCyclicallyReduced L ↔ IsReduced L ∧ ∀ a ∈ L.getLast?, ∀ b ∈ L.head?, a.1 = b.1 → a.2 = b.2

theorem FreeAddGroup.isCyclicallyReduced_iff {α : Type u} {L : List (α × Bool)} : IsCyclicallyReduced L ↔ IsReduced L ∧ ∀ a ∈ L.getLast?, ∀ b ∈ L.head?, a.1 = b.1 → a.2 = b.2

theorem FreeGroup.isCyclicallyReduced_cons_append_iff {α : Type u} {L : List (α × Bool)} {a b : α × Bool} : IsCyclicallyReduced (b :: L ++ [a]) ↔ IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)

theorem FreeAddGroup.isCyclicallyReduced_cons_append_iff {α : Type u} {L : List (α × Bool)} {a b : α × Bool} : IsCyclicallyReduced (b :: L ++ [a]) ↔ IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)

@[simp]

theorem FreeGroup.IsCyclicallyReduced.nil {α : Type u} : IsCyclicallyReduced []

@[simp]

theorem FreeAddGroup.IsCyclicallyReduced.nil {α : Type u} : IsCyclicallyReduced []

@[simp]

theorem FreeGroup.IsCyclicallyReduced.singleton {α : Type u} {x : α × Bool} : IsCyclicallyReduced [x]

@[simp]

theorem FreeAddGroup.IsCyclicallyReduced.singleton {α : Type u} {x : α × Bool} : IsCyclicallyReduced [x]

theorem FreeGroup.IsCyclicallyReduced.isReduced {α : Type u} {L : List (α × Bool)} (h : IsCyclicallyReduced L) : IsReduced L

theorem FreeAddGroup.IsCyclicallyReduced.isReduced {α : Type u} {L : List (α × Bool)} (h : IsCyclicallyReduced L) : IsReduced L

theorem FreeGroup.IsCyclicallyReduced.flatten_replicate {α : Type u} {L : List (α × Bool)} (n : ℕ) (h : IsCyclicallyReduced L) : IsCyclicallyReduced (List.replicate n L).flatten

theorem FreeAddGroup.IsCyclicallyReduced.flatten_replicate {α : Type u} {L : List (α × Bool)} (n : ℕ) (h : IsCyclicallyReduced L) : IsCyclicallyReduced (List.replicate n L).flatten