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