Elementary facts about Coxeter matrices

This file gives convenient equations for entries of Mathlib's type-A Coxeter matrix.

theorem TauCeti.coxeterMatrixA_apply {m : ℕ} (i j : Fin m) : (CoxeterMatrix.A m).M i j = if i = j then 1 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2

The entries of Mathlib's type-A Coxeter matrix, unfolded.

theorem TauCeti.coxeterMatrixA_eq_three {m : ℕ} {i j : Fin m} (h : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i) : (CoxeterMatrix.A m).M i j = 3

Neighbouring indices of the type-A Coxeter matrix carry the entry 3.

theorem TauCeti.coxeterMatrixA_eq_two {m : ℕ} {i j : Fin m} (h : ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i) : (CoxeterMatrix.A m).M i j = 2

Indices of the type-A Coxeter matrix at distance at least two carry the entry 2.