cartanMatrix_apply_eq_zero_iff — Mathlib

English

A Cartan matrix entry equals zero precisely when the corresponding root pairing vanishes.

Русский

Элемент Cartan(i,j) равен нулю тогда и только тогда, когда соответствующее парирование корней равно нулю.

LaTeX

$$$b.cartanMatrix i j = 0 \\iff P.pairing i j = 0$$$

Lean4

theorem cartanMatrix_apply_eq_zero_iff {i j : b.support} (hij : i ≠ j) :
    b.cartanMatrix i j = 0 ↔ P.root i + P.root j ∉ range P.root :=
  by
  rw [b.cartanMatrix_eq_neg_chainTopCoeff hij, neg_eq_zero, Int.natCast_eq_zero, P.chainTopCoeff_eq_zero_iff]
  replace hij := b.linearIndependent_pair_of_ne hij.symm
  tauto

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