ofPolynomial — Mathlib

English

The nth leading coefficient of an ideal of polynomials corresponds to the image under the lcoeff map of the i-th degree piece.

Русский

Порядковая ведущая коэффициентная часть для идеала полиномов соответствует образу подмодуля по полю lcoeff.

LaTeX

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

Lean4

/-- Transport an ideal of `R[X]` to an `R`-submodule of `R[X]`. -/
def ofPolynomial (I : Ideal R[X]) : Submodule R R[X]
    where
  carrier := I.carrier
  zero_mem' := I.zero_mem
  add_mem' := I.add_mem
  smul_mem' c x
    H := by
    rw [← C_mul']
    exact I.mul_mem_left _ H

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