def TypeABridge.glnCoxeterMatrixA (n : ℕ) : Matrix (Fin n) (Fin n) ℕ

The explicit numeric matrix for the type-$A$ Coxeter system on $\operatorname{Fin}(n)$.

theorem TypeABridge.glnCoxeterMatrixA_eq_typeA (n : ℕ) : glnCoxeterMatrixA n = (CoxeterMatrix.A n).M

The bare matrix glnCoxeterMatrixA n agrees with the underlying matrix of CoxeterMatrix.A n.