Theorems · Definition · group theory

CoxeterSystem.IsReflection

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

t : W is a reflection of the Coxeter system cs if it is of the form $w s_i w^{-1}$, where $w \in W$ and $s_i$ is a simple reflection.

Defined in

Mathlib.GroupTheory.Coxeter.Inversion

Cited by

17 results in Mathlib

Foundations

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

Assumes

Group