leadingCoeff_map — Mathlib

English

For any injective ring hom f, leadingCoeff(p.map f) = f(leadingCoeff p).

Русский

Для любого инъективного гомоморфизма f ведущий коэффициент многочлена после отображения равен образу ведущего коэффициента исходного многочлена.

LaTeX

$$$\operatorname{leadingCoeff}(p.map f) = f(\operatorname{leadingCoeff}(p)).$$$

Lean4

@[simp]
theorem leadingCoeff_map [Semiring S] [Nontrivial S] (f : R →+* S) : leadingCoeff (p.map f) = f (leadingCoeff p) := by
  simp only [← coeff_natDegree, coeff_map f, natDegree_map]

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