F₄ — Mathlib

English

The Cartan matrix of type F4 is the 4×4 integer matrix representing the F4 Dynkin diagram with a double bond.

Русский

Картанова матрица типа F4 — это 4×4 целочисленная матрица, задающая диаграмму F4 с двойной связью.

LaTeX

$$$F_4 = \\begin{pmatrix}2 & -1 & 0 & 0\\\\ -1 & 2 & -2 & 0\\\\ 0 & -1 & 2 & -1\\\\ 0 & 0 & -1 & 2\\end{pmatrix}$$$

Lean4

/-- The Cartan matrix of type f₄. See [bourbaki1968] plate VIII, page 288.

The corresponding Dynkin diagram is:
```
o --- o =>= o --- o
```
-/
def F₄ : Matrix (Fin 4) (Fin 4) ℤ :=
  !![2, -1, 0, 0; -1, 2, -2, 0; 0, -1, 2, -1; 0, 0, -1, 2]

Похожие утверждения