English
Let b be a crystallographic Cartan pairing base. For any i, j in the support of b, the absolute value of the Cartan matrix entry equals 4 on the diagonal adjusted by the diagonal entry, and equals the negated off-diagonal entry: |(b.cartanMatrix)_{i j}| = (4 if i = j else 0) − (b.cartanMatrix)_{i j}. In particular, for i ≠ j, |(b.cartanMatrix)_{i j}| = −(b.cartanMatrix)_{i j} and for i = j, |(b.cartanMatrix)_{i i}| = 4 − (b.cartanMatrix)_{i i}.
Русский
Пусть b — базис точного взаимно-однозначного сопряжённого корневого набора; для любых i, j из поддержки b модульная Картанова матрица удовлетворяет: |(b.cartanMatrix)_{i j}| = (4, если i = j; иначе 0) − (b.cartanMatrix)_{i j}. В частности, для i ≠ j выполняется |a_{i j}| = −a_{i j}, а для i = j — |a_{i i}| = 4 − a_{i i}.
LaTeX
$$$|\big(b.cartanMatrix\big)_{ij}| = \begin{cases}4 - \big(b.cartanMatrix\big)_{ii}, & i=j \\ -\big(b.cartanMatrix\big)_{ij}, & i\neq j\end{cases}$$$
Lean4
theorem abs_cartanMatrix_apply [DecidableEq ι] {i j : b.support} :
|b.cartanMatrix i j| = (if i = j then 4 else 0) - b.cartanMatrix i j :=
by
rcases eq_or_ne i j with rfl | h
· simp
· simpa [h] using b.cartanMatrix_le_zero_of_ne i j h
