English
The Coxeter matrix of type A_n is defined by M_{ii}=1 and M_{ij}=3 if |i-j|=1, else M_{ij}=2.
Русский
Коксетерова матрица типа A_n задаётся так: M_{ii}=1, а если |i-j|=1 то M_{ij}=3, иначе M_{ij}=2.
LaTeX
$$$$ M_{ij} = \\begin{cases}1,& i=j, \\\\ 3,& |i-j|=1, \\\\ 2,& \\text{иначе}. \\end{cases} \\quad \\text{для } i,j \\in \\{1,\\dots,n\\}. $$$$
Lean4
/-- The Coxeter matrix of type Aₙ.
The corresponding Coxeter-Dynkin diagram is:
```
o --- o --- o ⬝ ⬝ ⬝ ⬝ o --- o
```
-/
def Aₙ : CoxeterMatrix (Fin n)
where
M := Matrix.of fun i j : Fin n ↦ if i = j then 1 else (if (j : ℕ) + 1 = i ∨ (i : ℕ) + 1 = j then 3 else 2)
isSymm := by unfold Matrix.IsSymm; aesop
diagonal := by simp
off_diagonal := by aesop
