mem_roots_sub_C — Mathlib

English

If p ∈ R[X] has positive degree and a ∈ R, then x ∈ (p − C a).roots iff p.eval x = a.

Русский

Если deg(p) > 0 и a ∈ R, тогда x ∈ (p − C a).roots эквивалентно p.eval x = a.

LaTeX

$$$ 0 < \deg p \Rightarrow \ bigl( x \in (p - C a).roots \iff p.eval x = a \bigr) $$$

Lean4

theorem mem_roots_sub_C {p : R[X]} {a x : R} (hp0 : 0 < degree p) : x ∈ (p - C a).roots ↔ p.eval x = a :=
  mem_roots_sub_C'.trans <| and_iff_right fun hp => hp0.not_ge <| hp.symm ▸ degree_C_le

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