R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : degree (f - g) < ↑(Finset.card s)
eval_fg : ∀ (x : R), x ∈ s → eval x f = eval x g
⊢ f - g = 0
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : degree (f - g) < ↑(Finset.card s)
eval_fg : ∀ (x : R), x ∈ s → eval x f = eval x g
⊢ f = g
rw [← sub_eq_zero]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : degree (f - g) < ↑(Finset.card s)
eval_fg : ∀ (x : R), x ∈ s → eval x f = eval x g
⊢ ∀ (x : R), x ∈ s → eval x (f - g) = 0
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : degree (f - g) < ↑(Finset.card s)
eval_fg : ∀ (x : R), x ∈ s → eval x f = eval x g
⊢ f - g = 0
refine' eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_fg_lt _
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : degree (f - g) < ↑(Finset.card s)
eval_fg : ∀ (x : R), x ∈ s → eval x f = eval x g
⊢ ∀ (x : R), x ∈ s → eval x f = eval x g
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : degree (f - g) < ↑(Finset.card s)
eval_fg : ∀ (x : R), x ∈ s → eval x f = eval x g
⊢ ∀ (x : R), x ∈ s → eval x (f - g) = 0
simp_rw [eval_sub, sub_eq_zero]
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : degree (f - g) < ↑(Finset.card s)
eval_fg : ∀ (x : R), x ∈ s → eval x f = eval x g
⊢ ∀ (x : R), x ∈ s → eval x f = eval x g
exact eval_fg