cartanMatrixIn_mul_diagonal_eq — Mathlib

English

Restriction to rationals in a crystallographic root pairing yields a Rat-root-system with the same root data, encoded via an appropriate base change.

Русский

Ограничение до рациональных в кристаллографической паре корней даёт Rat-корневую систему с теми же корневыми данными.

LaTeX

$$$\\text{restrictScalarsRat} : RootPairing ι \\mathbb{Q} (span_{\\mathbb{Q}}(range\\ P.root)) (span_{\\mathbb{Q}}(range\\ P.coroot))$$$

Lean4

theorem cartanMatrixIn_mul_diagonal_eq {P : RootSystem ι R M N} [P.IsValuedIn S] (B : P.InvariantForm) (b : P.Base)
    [DecidableEq ι] :
    (b.cartanMatrixIn S).map (algebraMap S R) * (Matrix.diagonal fun i : b.support ↦ B.form (P.root i) (P.root i)) =
      (2 : R) • BilinForm.toMatrix b.toWeightBasis B.form :=
  by
  ext
  simp [B.two_mul_apply_root_root]

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