leadingCoeff — Mathlib

English

For an ideal I in the polynomial ring R[X], the ideal in R generated by all leading coefficients of polynomials in I is defined as the join of the subideals I.leadingCoeffNth n over all n ∈ N.

Русский

Для идеала I в кольце полиномов R[X] элемент в R, порожденный всеми лидирующими коэффициентами многочленов из I, задаётся как объединение (верхняя граница) подидеалов I.leadingCoeffNth n по всем n ∈ N.

LaTeX

$$$\\mathrm{leadingCoeff}(I) = \\bigvee_{n \\in \\mathbb{N}} I_{\\text{leadingCoeffNth } n}$$$

Lean4

/-- Given an ideal `I` in `R[X]`, make the ideal in `R` of the
leading coefficients in `I`. -/
def leadingCoeff : Ideal R :=
  ⨆ n : ℕ, I.leadingCoeffNth n

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