Theorems · Theorem · group theory

FreeAddGroup.reduceCyclically.reduce_flatten_replicate_succ

∀ {α : Type u} {L : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.IsReduced L →
    ∀ (n : ℕ),
      FreeAddGroup.reduce (List.replicate (n + 1) L).flatten =
        FreeAddGroup.reduceCyclically.conjugator L ++
            (List.replicate (n + 1) (FreeAddGroup.reduceCyclically L)).flatten ++
          FreeAddGroup.negRev (FreeAddGroup.reduceCyclically.conjugator L)

Defined in

Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Cited by

1 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq