English
If injOn v on s and deg f ≤ |s| and deg f = deg g and f(v(i)) = g(v(i)) for all i ∈ s, then f = g.
Русский
Если injOn v на s и deg f ≤ |s| и deg f = deg g и f(v(i)) = g(v(i)) для всех i ∈ s, то f = g.
LaTeX
$$$$\\mathrm{injOn}(v,s) \\Rightarrow (\\deg f \\le |s|) \\Rightarrow (\\deg f = \\deg g) \\Rightarrow (\\forall i \\in s, f(v(i)) = g(v(i))) \\Rightarrow f=g.$$$$
Lean4
theorem eq_of_degree_le_of_eval_index_eq (hvs : Set.InjOn v s) (h_deg_le : f.degree ≤ #s)
(h_deg_eq : f.degree = g.degree) (hlc : f.leadingCoeff = g.leadingCoeff)
(h_eval : ∀ i ∈ s, f.eval (v i) = g.eval (v i)) : f = g :=
by
rcases eq_or_ne f 0 with rfl | hf
· rwa [degree_zero, eq_comm, degree_eq_bot, eq_comm] at h_deg_eq
· exact eq_of_degree_sub_lt_of_eval_index_eq s hvs (lt_of_lt_of_le (degree_sub_lt h_deg_eq hf hlc) h_deg_le) h_eval
