not_isRoot_C

Mathlib.Algebra.Polynomial.Eval.Defs

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

English

If r ≠ 0, then the constant polynomial C(r) has no roots; in particular, for every a, (C(r))(a) ≠ 0.

Русский

Если r ≠ 0, то константный полином C(r) не имеет корней; в частности, для любого a выполняется (C(r))(a) ≠ 0.

LaTeX

$$$r \\neq 0 \\Rightarrow \\forall a\\, (C(r))(a) \\neq 0$$$

Lean4

theorem not_isRoot_C (r a : R) (hr : r ≠ 0) : ¬IsRoot (C r) a := by simpa using hr

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

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

Разделы

Аффилиация

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