IsRoot

Mathlib.Algebra.Polynomial.Eval.Defs

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

English

IsRoot(p, a) is the predicate that the evaluation of p at a equals zero, i.e., p.eval a = 0.

Русский

IsRoot(p, a) — это предикат, равный тому, что p(a) = 0, то есть p.eval a = 0.

LaTeX

$$$ \mathrm{IsRoot}(p,a) \equiv p.eval a = 0 $$$

Lean4

/-- `IsRoot p x` implies `x` is a root of `p`. The evaluation of `p` at `x` is zero -/
def IsRoot (p : R[X]) (a : R) : Prop :=
  p.eval a = 0

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

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

Разделы

Аффилиация

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