aeval_mem_adjoin_singleton

Mathlib.RingTheory.Adjoin.Polynomial

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

English

For any polynomial p, the evaluation aeval x p lies in the subalgebra generated by x.

Русский

Для любого многочлена p значение aeval x p принадлежит подалгебре, порождаемой x.

LaTeX

$$$\\mathit{aeval}_x(p) \\in \\operatorname{adjoin}_R\\{x\\}$$$

Lean4

@[simp]
theorem aeval_mem_adjoin_singleton : aeval x p ∈ adjoin R { x } := by simp [adjoin_singleton_eq_range_aeval]

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

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

Разделы

Аффилиация

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