coroot_mem_span_int

Mathlib.LinearAlgebra.RootSystem.Base

URI: https://scilib.ai/kg/mathlib#RootPairing.Base.coroot_mem_span_int

English

For each i, the coroot i lies in the span over the integers of P.coroot '' b.support.

Русский

Для каждого i корорт P.coroot i лежит в целочисленной оболочке P.coroot '' b.support.

LaTeX

$$$P.coroot_i \\in \\operatorname{span}_{\\mathbb{Z}}(P.coroot '' b.support).$$$

Lean4

theorem coroot_mem_span_int (i : ι) : P.coroot i ∈ span ℤ (P.coroot '' b.support) :=
  b.flip.root_mem_span_int i

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru