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