mem_roots_iff — Mathlib

English

For an integral domain R, x is a root of P if and only if P(a) x^3 + P(b) x^2 + P(c) x + P(d) = 0, provided P.toPoly ≠ 0.

Русский

Для целочисленного поля R выполняется: x является корнем P тогда и только тогда, когда P(a) x^3 + P(b) x^2 + P(c) x + P(d) = 0, при условии P.toPoly ≠ 0.

LaTeX

$$$$\\text{mem_roots }(R)\\;: \\; x \\in P.roots \\iff P.a x^3 + P.b x^2 + P.c x + P.d = 0.$$$$

Lean4

theorem mem_roots_iff [IsDomain R] (h0 : P.toPoly ≠ 0) (x : R) :
    x ∈ P.roots ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0 :=
  by
  rw [roots, mem_roots h0, IsRoot, toPoly]
  simp only [eval_C, eval_X, eval_add, eval_mul, eval_pow]

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