h — Mathlib · SciLib

English

The matrix h is built as a block matrix with a diagonal block encoding the pairingIn data.

Русский

Матрица h строится как блочная матрица с диагональным блоком, кодирующим данные pairingIn.

LaTeX

$$h(i) = \\mathrm{fromBlocks}\\ 0\\ 0\\ 0\\ \\mathrm{diag}(P.pairingIn \\mathbb{Z} \\cdot i)$$

Lean4

/-- Part of an `sl₂` triple used in Geck's construction of a Lie algebra from a root system. -/
def h (i : b.support) : Matrix (b.support ⊕ ι) (b.support ⊕ ι) R :=
  open scoped Classical in .fromBlocks 0 0 0 (.diagonal (P.pairingIn ℤ · i))

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