cartanMatrix_apply_same — Mathlib

English

For the diagonal entries against a base, the Cartan matrix equals 2, reflecting the normalization of a root with itself.

Русский

Для диагональных элементов матрица Каррана равна 2, что соответствует нормировке корня по отношению к самому себе.

LaTeX

$$$b.cartanMatrix i i = 2$ for all i$$

Lean4

theorem cartanMatrix_apply_same (i : b.support) : b.cartanMatrix i i = 2 :=
  b.cartanMatrixIn_apply_same ℤ i

Похожие утверждения