span_int_coroot_support — Mathlib

English

Let P be a RootPairing with a base b. Then the integer-span of the coroots corresponding to the indices in the support of b coincides with the integer-span of all coroots; equivalently, the ℤ-span of {P.coroot(i) : i ∈ b.support} equals the ℤ-span of {P.coroot(i) : i ∈ ι}.

Русский

Пусть P — корневое развёртывание с базисом b. Тогда целочисленная линейная оболочка коротов, индексируемых по поддержке b, совпадает с оболочкой всех коротов; т.е. span_ℤ{P.coroot(i) | i ∈ b.support} = span_ℤ{P.coroot(i) | i ∈ ι}.

LaTeX

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

Lean4

@[simp]
theorem span_int_coroot_support : span ℤ (P.coroot '' b.support) = span ℤ (range P.coroot) :=
  b.flip.span_int_root_support

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