cartanMatrix_apply_eq_zero_iff_symm

English

The zero-criterion is symmetric in i and j: cartanMatrix(i,j)=0 iff cartanMatrix(j,i)=0.

Русский

Критерий нулевой симметрии по индексу: Cartan(i,j)=0 тогда и только тогда Cartan(j,i)=0.

LaTeX

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

Lean4

theorem cartanMatrix_apply_eq_zero_iff_symm {i j : b.support} : b.cartanMatrix i j = 0 ↔ b.cartanMatrix j i = 0 :=
  by
  have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
  simp only [cartanMatrix_apply_eq_zero_iff_pairing, P.pairing_eq_zero_iff]

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