@[reducible, inline]

abbrev CoxeterMatrix.typeA (n : ℕ) : CoxeterMatrix (Fin n)

The Coxeter matrix of type $A_{n-1}$ (linear Dynkin diagram with $n$ nodes).

@[reducible, inline]

abbrev CoxeterMatrix.typeC (n : ℕ) : CoxeterMatrix (Fin n)

The Coxeter matrix of type $C_n$ (also denoted $B_n$ in Mathlib): hyperoctahedral group.

@[reducible, inline]

abbrev CoxeterMatrix.typeD (n : ℕ) : CoxeterMatrix (Fin n)

The Coxeter matrix of type $D_n$ (fork at one end).

theorem CoxeterMatrix.typeA_matrix_formula (n : ℕ) (i j : Fin n) : (typeA n).M i j = if i = j then 1 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2

Explicit formula for the type-$A$ Coxeter matrix entries: $1$ on the diagonal, $3$ on the off-diagonal at adjacent indices, $2$ otherwise.

def CoxeterMatrix.typeAffinA (n : ℕ) : CoxeterMatrix (Fin (n + 1))

The affine type-$\tilde A_n$ Coxeter matrix: linear diagram on $n+1$ nodes wrapped into a cycle.

noncomputable def CoxeterMatrix.equiv_perm_mulEquiv_coxeterGroup_typeA (n : ℕ) : Equiv.Perm (Fin (n + 1)) ≃* (typeA n).Group

The Coxeter group of type $A_{n-1}$ is the symmetric group $S_n = \operatorname{Perm}(\operatorname{Fin}(n+1))$.

noncomputable def CoxeterMatrix.typeA_coxeterSystem (n : ℕ) : CoxeterSystem (typeA n) (Equiv.Perm (Fin (n + 1)))

The canonical Coxeter system structure on $S_n$ for type $A_{n-1}$.

noncomputable def CoxeterMatrix.typeC_signedPermGroup_mulEquiv (n : ℕ) : SignedPerm.SignedPermGroup n ≃* (typeC n).Group

The Coxeter group of type $C_n$ is the signed permutation group $S_n^\pm = (\{\pm 1\})^n \rtimes S_n$.

noncomputable def CoxeterMatrix.typeC_coxeterSystem (n : ℕ) : CoxeterSystem (typeC n) (SignedPerm.SignedPermGroup n)

The canonical Coxeter system structure on the signed permutation group for type $C_n$.

def affinBCond (i j : ℕ) : Prop

Adjacency predicate encoding the edges of the affine type-$\tilde B_n$ Dynkin diagram.

@[implicit_reducible]

instance instDecidableAffinBCond (i j : ℕ) : Decidable (affinBCond i j)

The affine-$B$ adjacency predicate is decidable.

theorem affinBCond_comm (i j : ℕ) : affinBCond i j ↔ affinBCond j i

The affine-$B$ adjacency predicate is symmetric in its arguments.

def affinDCond (n i j : ℕ) : Prop

Adjacency predicate encoding the edges of the affine type-$\tilde D_n$ Dynkin diagram.

@[implicit_reducible]

instance instDecidableAffinDCond (n i j : ℕ) : Decidable (affinDCond n i j)

The affine-$D$ adjacency predicate is decidable.

theorem affinDCond_comm (n i j : ℕ) : affinDCond n i j ↔ affinDCond n j i

The affine-$D$ adjacency predicate is symmetric in $i$ and $j$.

def CoxeterMatrix.typeAffinB (n : ℕ) : CoxeterMatrix (Fin (n + 1))

The affine type-$\tilde B_n$ Coxeter matrix.

def CoxeterMatrix.typeAffinC (n : ℕ) : CoxeterMatrix (Fin (n + 1))

The affine type-$\tilde C_n$ Coxeter matrix.

def CoxeterMatrix.typeAffinD (n : ℕ) : CoxeterMatrix (Fin (n + 1))

The affine type-$\tilde D_n$ Coxeter matrix.