Polynomials are equal if they agree on a large enough set

Stream: Is there code for X?

[Thomas Waring]

Is this result in the library somewhere?

import Mathlib.Algebra.Polynomial.Roots

namespace Polynomial

theorem eq_of_natDegree_lt_card_of_eval_eq {R : Type*} [CommRing R] [IsDomain R]
    (p q : R[X]) {ι : Type*} [Fintype ι] (f : ι → R) (hf : Function.Injective f)
    (heval : ∀ i : ι, eval (f i) p = eval (f i) q)
    (hcard : max p.natDegree q.natDegree < Fintype.card ι) : p = q := by
  rw [←sub_eq_zero]
  apply eq_zero_of_natDegree_lt_card_of_eval_eq_zero (hf := hf)
  · simpa [sub_eq_zero]
  · grind [natDegree_sub_le]

the imported file has the equivalent result for two polynomials agreeing on an infinite set — docs#Polynomial.eq_of_infinite_eval_eq

[Snir Broshi]

You can use docs#Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero with p - q
nvm