degreeLT — Mathlib

English

Let R be a semiring. The R-submodule degreeLT(R, n) consists of polynomials in R[X] whose degree is strictly less than n.

Русский

Пусть R — полускольник. Подмодуль degreeLT(R, n) состоит из многочленов над R, степень которых строго меньше n.

LaTeX

$$$\operatorname{degreeLT}_R(n) = \{ f \in R[X] : \deg f < n \}$$$

Lean4

/-- The `R`-submodule of `R[X]` consisting of polynomials of degree < `n`. -/
def degreeLT (n : ℕ) : Submodule R R[X] :=
  ⨅ k : ℕ, ⨅ (_ : k ≥ n), LinearMap.ker (lcoeff R k)

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