leadingCoeffNth — Mathlib

English

Equivalently, the nth leading coefficient of an ideal I after restriction is the image under lcoeff of the nth degree piece.

Русский

Эквивалентно, ведущий коэффициент на позицию n полинома после ограничения является образ подстановки lcoeff от n-й степени части.

LaTeX

$$$I.\\operatorname{leadingCoeffNth}(n) = \\operatorname{map}(\\operatorname{Polynomial.lcoeff}(R,n))(I.\\operatorname{degreeLE}(n))$$$

Lean4

/-- Given an ideal `I` of `R[X]`, make the ideal in `R` of
leading coefficients of polynomials in `I` with degree ≤ `n`. -/
def leadingCoeffNth (n : ℕ) : Ideal R :=
  (I.degreeLE n).map <| lcoeff R n

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