Equality_of_Polynomials
Provedequalitypolynomialproofwikiring-theory
and are equal as polynomials and are equal as functions. Thus we can say without ambiguity as to what it means.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.RingTheory.Polynomial.Basic
Formal statement
theorem Equality_of_Polynomials {R : Type _} [CommRing R] [IsDomain R] [Infinite R] (f g : Polynomial R) : (∀ x : R, f.eval x = g.eval x) → f = g := by sorrySource