aeval_eq_zero_of_mem_rootSet

Mathlib.Algebra.Polynomial.Roots

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

← MathLib Explorer

English

If a is a root of p in S, then f(a) is a root of p in S'.

Русский

Если a является корнем p в S, то f(a) является корнем p в S'.

LaTeX

$$$$ (p.rootSet S).MapsTo f (p.rootSet S') $$$$

Lean4

theorem aeval_eq_zero_of_mem_rootSet {p : T[X]} [CommRing S] [IsDomain S] [Algebra T S] {a : S} (hx : a ∈ p.rootSet S) :
    aeval a p = 0 :=
  (mem_rootSet'.1 hx).2

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

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

Разделы

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

Аффилиация

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