English
If deg f ≤ |s|, deg f = deg g, and f and g agree on s, then f = g.
Русский
Если deg f ≤ |s|, deg f = deg g и f и g совпадают на s, то f = g.
LaTeX
$$$$\\deg f \\le |s|,\\; \\deg f = \\deg g,\\; f_{\\text{lead}} = g_{\\text{lead}} \\Rightarrow f = g.$$$$
Lean4
/-- Two polynomials, with the same degree and leading coefficient, which have the same evaluation
on a set of distinct values with cardinality equal to the degree, are equal.
-/
theorem eq_of_degree_le_of_eval_finset_eq (h_deg_le : f.degree ≤ #s) (h_deg_eq : f.degree = g.degree)
(hlc : f.leadingCoeff = g.leadingCoeff) (h_eval : ∀ x ∈ s, f.eval x = g.eval x) : 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_finset_eq s (lt_of_lt_of_le (degree_sub_lt h_deg_eq hf hlc) h_deg_le) h_eval
