root_mem_span_int — Mathlib

English

For each i, the root i lies in the span over the integers of P.root applied to b.support.

Русский

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

LaTeX

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

Lean4

theorem root_mem_span_int (i : ι) : P.root i ∈ span ℤ (P.root '' b.support) :=
  by
  have := b.root_mem_or_neg_mem i
  simp only [← span_nat_eq_addSubmonoidClosure, mem_toAddSubmonoid] at this
  rw [← span_span_of_tower (R := ℕ)]
  rcases this with hi | hi
  · exact subset_span hi
  · rw [← neg_mem_iff]
    exact subset_span hi

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