isRoot_of_eval₂_map_eq_zero

Mathlib.Algebra.Polynomial.AlgebraMap

URI: https://scilib.ai/kg/mathlib#Polynomial.isRoot_of_eval₂_map_eq_zero

← MathLib Explorer

English

If f is injective and eval₂ f (f r) p = 0, then p has r as a root.

Русский

Если f инъективен и eval₂ f (f r) p = 0, тогда r является корнем p.

LaTeX

$$hf : Injective f → eval₂ f (f r) p = 0 → p.IsRoot r$$

Lean4

theorem isRoot_of_eval₂_map_eq_zero (hf : Function.Injective f) {r : R} : eval₂ f (f r) p = 0 → p.IsRoot r :=
  by
  intro h
  apply hf
  rw [← eval₂_hom, h, f.map_zero]

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

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

Разделы

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

Аффилиация

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