allCoeffs — Mathlib

English

The list of all roots equals the list of all integer linear combinations of shortRoot and longRoot with coefficients from allCoeffs.

Русский

Список всех корней равен списку всех целочисленных линейных комбинаций shortRoot и longRoot с коэффициентами из allCoeffs.

LaTeX

$$$\text{allRoots}(P) = \text{map}_{\text{coeffs}}(\text{shortRoot}(P),\text{longRoot}(P),\text{allCoeffs})$$$

Lean4

/-- The coefficients of each root in the `𝔤₂` root pairing, relative to the base. -/
abbrev allCoeffs : List (Fin 2 → ℤ) :=
  [![0, 1], ![0, -1], ![1, 0], ![-1, 0], ![1, 1], ![-1, -1], ![2, 1], ![-2, -1], ![3, 1], ![-3, -1], ![3, 2], ![-3, -2]]

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