Theorems · Definition · group theory

CoxeterSystem.wordProd

{B : Type u_1} → {W : Type u_3} → [inst : Group W] → {M : CoxeterMatrix B} → CoxeterSystem M W → List B → W

The product of the simple reflections of W corresponding to the indices in ω.

Defined in

Mathlib.GroupTheory.Coxeter.Basic

Cited by

42 results in Mathlib

Foundations

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

Assumes

Group