degreeLE — Mathlib

English

For any ideal I of R[X], the degreeLE construction equals the minimum of the ambient polynomial degree and the polynomial ideal I.

Русский

Для идеала I над R[X] конструкция degreeLE равна минимуму степени полинома и I.

LaTeX

$$$I.\\operatorname{degreeLE}(n) = \\min\\{ \\operatorname{Polynomial.degreeLE}(R,n), I.\\mathrm{ofPolynomial} \\}$$$

Lean4

/-- Given an ideal `I` of `R[X]`, make the `R`-submodule of `I`
consisting of polynomials of degree ≤ `n`. -/
def degreeLE (n : WithBot ℕ) : Submodule R R[X] :=
  Polynomial.degreeLE R n ⊓ I.ofPolynomial

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