H₃ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The Coxeter matrix of type H₃.

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

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