English
The Coxeter matrix of type E₈ is the 8×8 symmetric matrix with entries determined by the E₈ Dynkin diagram.
Русский
Коксетерова матрица типа E₈ — симметричная 8×8 матрица, значения которой соответствуют диаграмме E₈.
LaTeX
$$$$ M = \\begin{pmatrix} 1 & 2 & 3 & 2 & 2 & 2 & 2 & 2 \\\\ 2 & 1 & 2 & 3 & 2 & 2 & 2 & 2 \\\\ 3 & 2 & 1 & 3 & 2 & 2 & 2 & 2 \\\\ 2 & 3 & 3 & 1 & 3 & 2 & 2 & 2 \\\\ 2 & 2 & 2 & 3 & 1 & 3 & 2 & 2 \\\\ 2 & 2 & 2 & 2 & 3 & 1 & 3 & 2 \\\\ 2 & 2 & 2 & 2 & 2 & 3 & 1 & 3 \\\\ 2 & 2 & 2 & 2 & 2 & 2 & 3 & 1 \\ \\end{pmatrix}. $$$$
Lean4
/-- The Coxeter matrix of type E₈.
The corresponding Coxeter-Dynkin diagram is:
```
o
|
o --- o --- o --- o --- o --- o --- o
```
-/
def E₈ : CoxeterMatrix (Fin 8) where
M :=
!![1, 2, 3, 2, 2, 2, 2, 2;
2, 1, 2, 3, 2, 2, 2, 2;
3, 2, 1, 3, 2, 2, 2, 2;
2, 3, 3, 1, 3, 2, 2, 2;
2, 2, 2, 3, 1, 3, 2, 2;
2, 2, 2, 2, 3, 1, 3, 2;
2, 2, 2, 2, 2, 3, 1, 3;
2, 2, 2, 2, 2, 2, 3, 1]
