cartanMatrix_map_abs — Mathlib

English

For a crystallographic root system, applying the absolute value entrywise to the Cartan matrix yields the matrix 4I − Cartan, i.e., the absolute values of diagonal entries fit 4 minus the diagonal, and off-diagonal entries become the negation of the original entry.

Русский

Для кристаллической корневой системы применение поразрядному модуля к Картановой матрице даёт матрицу 4I − Cartan: по диагонали |a_{ii}| = 4 − a_{ii}, а вне диагонали |a_{ij}| = −a_{ij}.

LaTeX

$$$\operatorname{Abs}(b.cartanMatrix) = 4I - b.cartanMatrix$$$

Lean4

@[simp]
theorem cartanMatrix_map_abs [DecidableEq ι] : b.cartanMatrix.map abs = 4 - b.cartanMatrix := by ext;
  simp [abs_cartanMatrix_apply, Matrix.ofNat_apply]

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