algebraMap_cartanMatrixIn_apply — Mathlib

English

The restriction of scalars for a crystallographic root pairing yields a consistent RootSystemBase over K on the span of roots and coroots.

Русский

Ограничение скаляров для кристаллографической пары корней даёт согласованную RootSystemBase над K на линейном замке корней и коротов.

LaTeX

$$$\\text{restrictScalars} : RootSystem ι K (\\operatorname{span}_K(\\operatorname{range}(P.root))) (\\operatorname{span}_K(\\operatorname{range}(P.coroot)))$$$

Lean4

@[simp]
theorem algebraMap_cartanMatrixIn_apply (i j : b.support) : algebraMap S R (b.cartanMatrixIn S i j) = P.pairing i j :=
  by simp [cartanMatrixIn_def]

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