English
The Coxeter matrix of type F₄ is the 4×4 symmetric matrix with a heavier edge of weight 4 between a pair of adjacent nodes and other adjacencies of weight 3, with weight 2 elsewhere.
Русский
Коксетерова матрица типа F₄ — симметричная 4×4 матрица: имеется пара соседних узлов с весом 4, другие соседние пары — вес 3, остальные — вес 2.
LaTeX
$$$$ M = \\begin{pmatrix} 1 & 3 & 2 & 2 \\\\ 3 & 1 & 4 & 2 \\\\ 2 & 4 & 1 & 3 \\\\ 2 & 2 & 3 & 1 \\ \\end{pmatrix}. $$$$
Lean4
/-- The Coxeter matrix of type F₄.
The corresponding Coxeter-Dynkin diagram is:
```
4
o --- o --- o --- o
```
-/
def F₄ : CoxeterMatrix (Fin 4) where M := !![1, 3, 2, 2; 3, 1, 4, 2; 2, 4, 1, 3; 2, 2, 3, 1]
