English
The Cartan matrix of type E8 is the 8×8 integer matrix with the entries corresponding to the E8 Dynkin diagram.
Русский
Картанова матрица типа E8 — это 8×8 целочисленная матрица, соответствующая диаграмме E8 Дынки.
LaTeX
$$$E_8 = \\begin{pmatrix}2 & 0 & -1 & 0 & 0 & 0 & 0 & 0\\\\ 0 & 2 & 0 & -1 & 0 & 0 & 0 & 0\\\\ -1 & 0 & 2 & -1 & 0 & 0 & 0 & 0\\\\ 0 & -1 & -1 & 2 & -1 & 0 & 0 & 0\\\\ 0 & 0 & 0 & -1 & 2 & -1 & 0 & 0\\\\ 0 & 0 & 0 & 0 & -1 & 2 & -1 & 0\\\\ 0 & 0 & 0 & 0 & 0 & -1 & 2 & -1\\\\ 0 & 0 & 0 & 0 & 0 & 0 & -1 & 2\\end{pmatrix}$$$
Lean4
/-- The Cartan matrix of type e₈. See [bourbaki1968] plate VII, page 285.
The corresponding Dynkin diagram is:
```
o
|
o --- o --- o --- o --- o --- o --- o
```
-/
def E₈ : Matrix (Fin 8) (Fin 8) ℤ :=
!![2, 0, -1, 0, 0, 0, 0, 0;
0, 2, 0, -1, 0, 0, 0, 0;
-1, 0, 2, -1, 0, 0, 0, 0;
0, -1, -1, 2, -1, 0, 0, 0;
0, 0, 0, -1, 2, -1, 0, 0;
0, 0, 0, 0, -1, 2, -1, 0;
0, 0, 0, 0, 0, -1, 2, -1;
0, 0, 0, 0, 0, 0, -1, 2]
