span_root_support — Mathlib

English

For a base b of the root system and any root P.root(i) with i in the base support, the span over R of the roots in the support equals the overall root-span generated by all roots; i.e., span_R(P.root '' b.support) = P.rootSpan R.

Русский

Пусть базис системы корней b; тогда линейная оболочка корней с индексами из поддержки совпадает с оболочкой корней всей системы: span_R( {P.root(i) : i ∈ b.support} ) = rootSpan_R.

LaTeX

$$$\operatorname{span}_{R}(P.root '' b.support) = P.rootSpan R$$$

Lean4

@[simp]
theorem span_root_support : span R (P.root '' b.support) = P.rootSpan R := by
  rw [← span_span_of_tower (R := ℤ), span_int_root_support, span_span_of_tower]

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