eval_surjective

Mathlib.Algebra.Polynomial.Eval.Defs

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

English

For every x ∈ R, the evaluation map eval x : R[X] → R is surjective.

Русский

Для каждого x ∈ R отображение оценки eval_x: R[X] → R является сюръективным.

LaTeX

$$$\\forall y \\in R, \\exists p \\in R[X], \\; \\text{eval}_x(p) = y$$$

Lean4

theorem eval_surjective (x : R) : Function.Surjective <| eval x := fun y => ⟨C y, eval_C⟩

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

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

Разделы

Аффилиация

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