H₄ — Mathlib

English

Let M be the Coxeter matrix of type H₄. Then M is the 4×4 matrix M = [[1,3,2,2],[3,1,3,2],[2,3,1,5],[2,2,5,1]].

Русский

Пусть M — матрица Коксетера типа H₄. Тогда M — это матрица 4×4: [[1,3,2,2],[3,1,3,2],[2,3,1,5],[2,2,5,1]].

LaTeX

$$$M = \begin{pmatrix}1 & 3 & 2 & 2\\ 3 & 1 & 3 & 2\\ 2 & 3 & 1 & 5\\ 2 & 2 & 5 & 1\end{pmatrix}$$$

Lean4

/-- The Coxeter matrix of type H₄.

The corresponding Coxeter-Dynkin diagram is:
```
       5
    o --- o --- o --- o
```
-/
def H₄ : CoxeterMatrix (Fin 4) where M := !![1, 3, 2, 2; 3, 1, 3, 2; 2, 3, 1, 5; 2, 2, 5, 1]

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