map_scaleRoots — Mathlib

English

Let f be a ring homomorphism with f(p.leadingCoeff) ≠ 0. Then mapping scaleRoots commutes with map: (p.scaleRoots x).map f = (p.map f).scaleRoots (f x).

Русский

Пусть f — гомоморфизм колец с f(p.leadingCoeff) ≠ 0. Тогда отображение scaleRoots через f коммутирует с scaleRoots над отображением: (p.scaleRoots x).map f = (p.map f).scaleRoots (f x).

LaTeX

$$$\big( (\operatorname{scaleRoots}(p, x)) \map f \big) = \operatorname{scaleRoots}(p.map f, f x)$, при $f(p.leadingCoeff) \neq 0$$$

Lean4

theorem map_scaleRoots (p : R[X]) (x : R) (f : R →+* S) (h : f p.leadingCoeff ≠ 0) :
    (p.scaleRoots x).map f = (p.map f).scaleRoots (f x) :=
  by
  ext
  simp [Polynomial.natDegree_map_of_leadingCoeff_ne_zero _ h]

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