English
The span of a finite set of polynomials is contained in some degreeLE n.
Русский
Образование линейной оболочки конечного набора многочленов содержится в degreeLE n для некоторого n.
LaTeX
$$$\exists n \; Submodule.span_R s \le \operatorname{degreeLE}_R(n).$$$
Lean4
/-- For every polynomial `p` in the span of a set `s : Set R[X]`, there exists a polynomial of
`p' ∈ s` with higher degree. See also `Polynomial.exists_degree_le_of_mem_span_of_finite`. -/
theorem exists_degree_le_of_mem_span {s : Set R[X]} {p : R[X]} (hs : s.Nonempty) (hp : p ∈ Submodule.span R s) :
∃ p' ∈ s, degree p ≤ degree p' := by
by_contra! h
by_cases hp_zero : p = 0
· rw [hp_zero, degree_zero] at h
rcases hs with ⟨x, hx⟩
exact not_lt_bot (h x hx)
· have : p ∈ degreeLT R (natDegree p) :=
by
refine (Submodule.span_le.mpr fun p' p'_mem => ?_) hp
rw [SetLike.mem_coe, mem_degreeLT, Nat.cast_withBot]
exact lt_of_lt_of_le (h p' p'_mem) degree_le_natDegree
rwa [mem_degreeLT, Nat.cast_withBot, degree_eq_natDegree hp_zero, Nat.cast_withBot, lt_self_iff_false] at this
