mem_roots_sub_C' — Mathlib

English

For p ∈ R[X], a ∈ R, and x ∈ R, x is a root of p − C a iff p ≠ C a and p.eval x = a.

Русский

Для p ∈ R[X], a ∈ R и x ∈ R, x — корень p − C a тогда и только тогда, когда p ≠ C a и p.eval x = a.

LaTeX

$$$ {p:\,R[X]}\ {a,x:\,R} : x \in (p - C a).roots \iff p \neq C a \wedge p.eval x = a $$$

Lean4

theorem mem_roots_sub_C' {p : R[X]} {a x : R} : x ∈ (p - C a).roots ↔ p ≠ C a ∧ p.eval x = a := by
  rw [mem_roots', IsRoot.def, sub_ne_zero, eval_sub, sub_eq_zero, eval_C]

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