Theorems · Theorem · commutative algebra

Polynomial.exists_degree_le_of_mem_span

∀ {R : Type u} [inst : Semiring R] {s : Set (Polynomial R)} {p : Polynomial R},
  s.Nonempty → p ∈ Submodule.span R s → ∃ p' ∈ s, p.degree ≤ p'.degree

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.

Defined in

Mathlib.RingTheory.Polynomial.Basic

Cited by

1 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Semiring