cartanMatrix_eq_neg_chainTopCoeff

English

For i ≠ j, Cartan(i,j) equals the negation of the top coefficient of the j,i chain in the root system data.

Русский

Для i ≠ j Cartan(i,j) равен минусу верхнего коэффициента цепи j,i в данных корневой системы.

LaTeX

$$$b.cartanMatrix i j = -P.chainTopCoeff j i$ for i ≠ j$$

Lean4

theorem cartanMatrix_eq_neg_chainTopCoeff {i j : b.support} (hij : i ≠ j) : b.cartanMatrix i j = -P.chainTopCoeff j i :=
  by rw [cartanMatrix, cartanMatrixIn_def, ← neg_eq_iff_eq_neg, ← b.chainTopCoeff_eq_of_ne hij.symm]

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