map_roots — Mathlib

English

If φ is a ring homomorphism and P is a cubic over R, then the roots of the mapped cubic equal the image of the original polynomial's roots.

Русский

Если φ — гомоморфизм колец и P — кубический полином над R, тогда корни изображенного кубического полинома равны образам корней исходного полинома.

LaTeX

$$$$\\mathrm{roots}(\\mathrm{Cubic.map}\\,\\varphi\\,P) = \\mathrm{Polynomial.map}\\varphi\\,P.toPoly.\\text{roots}.$$$$

Lean4

theorem map_roots [IsDomain S] : (map φ P).roots = (Polynomial.map φ P.toPoly).roots := by rw [roots, map_toPoly]

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