Theorems · Definition · group theory

CoxeterSystem.length

{B : Type u_1} → {W : Type u_2} → [inst : Group W] → {M : CoxeterMatrix B} → CoxeterSystem M W → W → ℕ

The length of w; i.e., the minimum number of simple reflections that must be multiplied to form w.

Defined in

Mathlib.GroupTheory.Coxeter.Length

Cited by

41 results in Mathlib

Foundations

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

Assumes

Group