simple_determines_coxeterSystem — Mathlib

English

The wordProd of a sequence ω in B is the group product of the simple reflections indexed by ω.

Русский

Слово-произведение последовательности ω по индексам в B — это произведение простых отражений.

LaTeX

$$wordProd(ω) = ∏ cs.simple(ω_k)$$

Lean4

/-- 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. -/
theorem simple_determines_coxeterSystem : Injective (simple : CoxeterSystem M W → B → W) :=
  by
  intro cs1 cs2 h
  apply CoxeterSystem.ext
  apply MulEquiv.toMonoidHom_injective
  apply cs1.ext_simple
  intro i
  nth_rw 2 [h]
  simp [simple]

Похожие утверждения