theorem Polynomial.eq_of_eval_eq_degree {𝔽 : Type u_1} [Field 𝔽] {p q : Polynomial 𝔽} {n : ℕ} (hp : p.degree < ↑n) (hq : q.degree < ↑n) (s : Finset 𝔽) : s.card ≥ n → (∀ x ∈ s, eval x p = eval x q) → p = q

theorem Polynomial.eq_of_eval_eq_natDegree {𝔽 : Type u_1} [Field 𝔽] {p q : Polynomial 𝔽} {n : ℕ} (hp : p.natDegree < n) (hq : q.natDegree < n) (s : Finset 𝔽) : s.card ≥ n → (∀ x ∈ s, eval x p = eval x q) → p = q