R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R (Finset.card s)
degree_g_lt : g ∈ degreeLT R (Finset.card s)
eval_fg : ∀ (x : R), x ∈ s → eval x f = eval x g
⊢ f = g
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : degree f < ↑(Finset.card s)
degree_g_lt : degree g < ↑(Finset.card s)
eval_fg : ∀ (x : R), x ∈ s → eval x f = eval x g
⊢ f = g
rw [← mem_degreeLT] at degree_f_lt degree_g_lt
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R (Finset.card s)
degree_g_lt : g ∈ degreeLT R (Finset.card s)
eval_fg : ∀ (x : R), x ∈ s → eval x f = eval x g
⊢ degree (f - g) < ↑(Finset.card s)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R (Finset.card s)
degree_g_lt : g ∈ degreeLT R (Finset.card s)
eval_fg : ∀ (x : R), x ∈ s → eval x f = eval x g
⊢ f = g
refine' eq_of_degree_sub_lt_of_eval_finset_eq _ _ eval_fg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R (Finset.card s)
degree_g_lt : g ∈ degreeLT R (Finset.card s)
eval_fg : ∀ (x : R), x ∈ s → eval x f = eval x g
⊢ f - g ∈ degreeLT R (Finset.card s)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R (Finset.card s)
degree_g_lt : g ∈ degreeLT R (Finset.card s)
eval_fg : ∀ (x : R), x ∈ s → eval x f = eval x g
⊢ degree (f - g) < ↑(Finset.card s)
rw [← mem_degreeLT]
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R (Finset.card s)
degree_g_lt : g ∈ degreeLT R (Finset.card s)
eval_fg : ∀ (x : R), x ∈ s → eval x f = eval x g
⊢ f - g ∈ degreeLT R (Finset.card s)
exact Submodule.sub_mem _ degree_f_lt degree_g_lt