English
The Coxeter matrix of type D_n has M_{ii}=1; M_{i,i+1}=3 for adjacent pairs, with a fork-edge M_{n-3,n-1}=M_{n-1,n-3}=3 and M_{ij}=2 otherwise.
Русский
Коксетерова матрица типа D_n имеет M_{ii}=1; для соседних узлов M_{i,i+1}=3, для разветвления между n-3 и n-1 установлен вес 3, во всех остальных случаях 2.
LaTeX
$$$$ M_{ii}=1,\; M_{i,i+1}=3 \text{ для } i=1,\dots,n-2, \; M_{n-3,n-1}=M_{n-1,n-3}=3,\; M_{ij}=2 \text{ иначе}. $$$$
Lean4
/-- The Coxeter matrix of type Dₙ.
The corresponding Coxeter-Dynkin diagram is:
```
o
\
o --- o ⬝ ⬝ ⬝ ⬝ o --- o
/
o
```
-/
def Dₙ : CoxeterMatrix (Fin n)
where
M :=
Matrix.of fun i j : Fin n ↦
if i = j then 1
else
(if i = n - 1 ∧ j = n - 3 ∨ j = n - 1 ∧ i = n - 3 then 3
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
