lean_workbook_plus_14619
OpenProve that if two polynomials are equal for all real , then their coefficients must be the same.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14619 (p q : Polynomial ℝ) (h : ∀ x, p.eval x = q.eval x) : p = q := by sorry
Source