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_fg_lt : degree (f - g) < ↑(card s)
eval_fg : ∀ (i : ι), i ∈ s → eval (v i) f = eval (v i) g
⊢ f - g = 0
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_fg_lt : degree (f - g) < ↑(card s)
eval_fg : ∀ (i : ι), i ∈ s → eval (v i) f = eval (v i) g
⊢ f = g
rw [← sub_eq_zero]
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_fg_lt : degree (f - g) < ↑(card s)
eval_fg : ∀ (i : ι), i ∈ s → eval (v i) f = eval (v i) g
⊢ ∀ (i : ι), i ∈ s → eval (v i) (f - g) = 0
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_fg_lt : degree (f - g) < ↑(card s)
eval_fg : ∀ (i : ι), i ∈ s → eval (v i) f = eval (v i) g
⊢ f - g = 0
refine' eq_zero_of_degree_lt_of_eval_index_eq_zero _ hvs degree_fg_lt _
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_fg_lt : degree (f - g) < ↑(card s)
eval_fg : ∀ (i : ι), i ∈ s → eval (v i) f = eval (v i) g
⊢ ∀ (i : ι), i ∈ s → eval (v i) f = eval (v i) g
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_fg_lt : degree (f - g) < ↑(card s)
eval_fg : ∀ (i : ι), i ∈ s → eval (v i) f = eval (v i) g
⊢ ∀ (i : ι), i ∈ s → eval (v i) (f - g) = 0
simp_rw [eval_sub, sub_eq_zero]
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_fg_lt : degree (f - g) < ↑(card s)
eval_fg : ∀ (i : ι), i ∈ s → eval (v i) f = eval (v i) g
⊢ ∀ (i : ι), i ∈ s → eval (v i) f = eval (v i) g
exact eval_fg