coe_normUnit — Mathlib

English

For any polynomial p ∈ R[X], the polynomial corresponding to the normalization unit of p equals the constant polynomial given by the normalization of its leading coefficient: (normUnit p) as a polynomial = C ↑(normUnit p.leadingCoeff).

Русский

Для любого многочлена p ∈ R[X] соответствующий нормализационный единичный элемент p представляется как постоянный многочлен, равный нормализационному элементу ведущего коэффициента: (normUnit p) = C (normUnit p.leadingCoeff).

LaTeX

$$$ (\mathrm{normUnit}(p) : R[X]) = C( \mathrm{normUnit}(p_{\text{leadingCoeff}}) ). $$$

Lean4

@[simp]
theorem coe_normUnit {p : R[X]} : (normUnit p : R[X]) = C ↑(normUnit p.leadingCoeff) := by simp [normUnit]

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