of_map

Mathlib.Algebra.Polynomial.Eval.Coeff

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

← MathLib Explorer

English

From IsRoot (p.map f) (f x) and hf injective, deduce IsRoot p x.

Русский

Из IsRoot (p.map f) (f x) и инъективности hf следует IsRoot p x.

LaTeX

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

Lean4

theorem of_map {R} [Ring R] {f : R →+* S} {x : R} {p : R[X]} (h : IsRoot (p.map f) (f x)) (hf : Function.Injective f) :
    IsRoot p x := by rwa [IsRoot, ← (injective_iff_map_eq_zero' f).mp hf, ← eval₂_hom, ← eval_map]

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

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

Разделы

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

Аффилиация

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