span_of_finite_le_degreeLT — Mathlib

English

The span of any finite set of polynomials is contained in some degreeLT(R,n).

Русский

Образование любого конечного набора многочленов лежит в degreeLT(R,n) для некоторого n.

LaTeX

$$$\exists n \; \operatorname{span}_R s \le \operatorname{degreeLT}_R(n).$$$

Lean4

/-- The span of every finite set of polynomials is contained in a `degreeLT n` for some `n`. -/
theorem span_of_finite_le_degreeLT {s : Set R[X]} (s_fin : s.Finite) : ∃ n : ℕ, Submodule.span R s ≤ degreeLT R n :=
  by
  rcases span_le_degreeLE_of_finite s_fin with ⟨n, _⟩
  exact ⟨n + 1, by rwa [degreeLT_succ_eq_degreeLE]⟩

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