Theorems · Theorem · group theory

CoxeterSystem.listTake_succ_alternatingWord

∀ {B : Type u_1} (i j : B) (p k : ℕ),
  k + 1 < 2 * p →
    List.take (k + 1) (CoxeterSystem.alternatingWord i j (2 * p)) =
      i :: List.take k (CoxeterSystem.alternatingWord j i (2 * p))

Defined in

Mathlib.GroupTheory.Coxeter.Basic

Cited by

1 results in Mathlib

Foundations

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