span_int_root_support — Mathlib

English

The span over the integers of the roots is the same whether you take the images of b.support or the full range of P.root.

Русский

Оболочка целых чисел корней совпадает с образами b.support и всем диапазоном P.root.

LaTeX

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

Lean4

@[simp]
theorem span_int_root_support : span ℤ (P.root '' b.support) = span ℤ (range P.root) :=
  by
  refine le_antisymm (span_mono <| image_subset_range _ _) (span_le.mpr ?_)
  rintro - ⟨i, rfl⟩
  exact b.root_mem_span_int i

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