integralNormalization — Mathlib

English

The kernel of the evaluation-at x map on polynomials is the principal ideal generated by X − C x.

Русский

Ядро отображения оценки на x равно порождающему идеалу X − C x.

LaTeX

$$$\operatorname{ker}(\operatorname{evalRingHom} x) = \operatorname{Ideal}.span\{X - C x\}$$$

Lean4

/-- If `p : R[X]` is a nonzero polynomial with root `z`, `integralNormalization p` is
a monic polynomial with root `leadingCoeff f * z`.

Moreover, `integralNormalization 0 = 0`.
-/
noncomputable def integralNormalization (p : R[X]) : R[X] :=
  p.sum fun i a ↦ monomial i (if p.degree = i then 1 else a * p.leadingCoeff ^ (p.natDegree - 1 - i))

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