Theorems · Theorem · group theory

CoxeterSystem.simple_determines_coxeterSystem

∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B}, Function.Injective CoxeterSystem.simple

If two Coxeter systems on the same group W have the same Coxeter matrix M : Matrix B B ℕ and the same simple reflection map B → W, then they are identical.

Defined in

Mathlib.GroupTheory.Coxeter.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

Group