cartanMatrix — Mathlib

English

The Cartan matrix of a crystallographic root pairing with respect to a base b is a matrix with integer entries determined by the pairing data on the base roots.

Русский

Матрица Каррана кристаллографической пары корней относительно базиса b есть целочисленная матрица, определяемая данными спаривания между базисными корнями.

LaTeX

$$Cartan matrix := b.cartanMatrixIn ℤ$$

Lean4

/-- The Cartan matrix of a crystallographic root pairing, with respect to a base `b`. -/
abbrev cartanMatrix : Matrix b.support b.support ℤ :=
  b.cartanMatrixIn ℤ

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