English
The Cartan matrix of type G2 is a 2×2 integer matrix representing the G2 Dynkin diagram with a triple bond indicating unequal root lengths.
Русский
Картанова матрица типа G2 — это 2×2 целочисленная матрица, соответствующая диаграмме G2 с тройной связью, отражающей различие длин корней.
LaTeX
$$$G_2 = \\begin{pmatrix}2 & -3\\\\ -1 & 2\\end{pmatrix}$$$
Lean4
/-- The Cartan matrix of type g₂. See [bourbaki1968] plate IX, page 290.
The corresponding Dynkin diagram is:
```
o ≡>≡ o
```
Actually we are using the transpose of Bourbaki's matrix. This is to make this matrix consistent
with `CartanMatrix.F₄`, in the sense that all non-zero values below the diagonal are -1. -/
def G₂ : Matrix (Fin 2) (Fin 2) ℤ :=
!![2, -3; -1, 2]
