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