isRoot_map_iff

Mathlib.Algebra.Polynomial.Eval.Coeff

URI: https://scilib.ai/kg/mathlib#Polynomial.isRoot_map_iff

← MathLib Explorer

English

For injective f, IsRoot (p.map f) (f x) is equivalent to IsRoot p x.

Русский

При инъективном f равны условия IsRoot (p.map f) (f x) и IsRoot p x.

LaTeX

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

Lean4

theorem isRoot_map_iff {R : Type*} [CommRing R] {f : R →+* S} {x : R} {p : R[X]} (hf : Function.Injective f) :
    IsRoot (p.map f) (f x) ↔ IsRoot p x :=
  ⟨fun h => h.of_map hf, fun h => h.map⟩

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

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

Разделы

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

Аффилиация

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