eq_of_infinite_eval_eq — Mathlib

English

If polynomials p, q ∈ R[X] agree on infinitely many x ∈ R in the sense that eval x p = eval x q, then p = q.

Русский

Пусть p, q ∈ R[X]. Если их значения совпадают на бесконечно многих x ∈ R, то p = q.

LaTeX

$$$ (p,q:\,R[X])\,\text{ with infinite set }\{ x\in R \mid eval(x,p)=eval(x,q)\} \Rightarrow p=q $$$

Lean4

theorem eq_of_infinite_eval_eq (p q : R[X]) (h : Set.Infinite {x | eval x p = eval x q}) : p = q :=
  by
  rw [← sub_eq_zero]
  apply eq_zero_of_infinite_isRoot
  simpa only [IsRoot, eval_sub, sub_eq_zero]

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