map

Mathlib.Algebra.Polynomial.Eval.Coeff

URI: https://scilib.ai/kg/mathlib#Polynomial.IsRoot.map

← MathLib Explorer

English

If p is a root of x, then p.map f is a root of f x.

Русский

Если p корень в x, то p.map f корень в f x.

LaTeX

$$$ p.IsRoot\\ x \\Rightarrow (p.map f).IsRoot (f x) $$$

Lean4

theorem map {f : R →+* S} {x : R} {p : R[X]} (h : IsRoot p x) : IsRoot (p.map f) (f x) := by
  rw [IsRoot, eval_map, eval₂_hom, h.eq_zero, f.map_zero]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru