F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
degree_f_lt : degree f < ↑(card s)
eval_f : ∀ (i : ι), i ∈ s → eval (v i) f = r i
⊢ (↑(interpolate s v) fun i => eval (v i) f) = ↑(interpolate s v) r
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
degree_f_lt : degree f < ↑(card s)
eval_f : ∀ (i : ι), i ∈ s → eval (v i) f = r i
⊢ f = ↑(interpolate s v) r
rw [eq_interpolate hvs degree_f_lt]
no goals
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
degree_f_lt : degree f < ↑(card s)
eval_f : ∀ (i : ι), i ∈ s → eval (v i) f = r i
⊢ (↑(interpolate s v) fun i => eval (v i) f) = ↑(interpolate s v) r
exact interpolate_eq_of_values_eq_on _ _ eval_f