English
Let R be a semiring. For every n in WithBot ℕ, the R-submodule of R[X] consisting of polynomials of degree at most n is exactly the intersection of the kernels of the coefficient maps lcoeff R k for all k > n; equivalently, a polynomial f has degree ≤ n if and only if all coefficients of degree higher than n vanish.
Русский
Пусть R — полукольцо. Для каждого n в WithBot ℕ подмодуль R[X], состоящий из многочленов степени не больше n, есть точное равенство: это пересечение ядер отображений коэффициентов lcoeff R k по всем k > n; эквивалентно: deg f ≤ n тогда и только тогда, когда коэффициенты степени выше n равны нулю.
LaTeX
$$$\operatorname{degreeLE}_R(n) = \bigcap_{k>n} \ker\bigl(\operatorname{lcoeff} R k\bigr).$$$
Lean4
/-- The `R`-submodule of `R[X]` consisting of polynomials of degree ≤ `n`. -/
def degreeLE (n : WithBot ℕ) : Submodule R R[X] :=
⨅ k : ℕ, ⨅ _ : ↑k > n, LinearMap.ker (lcoeff R k)
