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