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