Epimorphism_from_Polynomial_Forms_to_Polynomial_Functions
Provedepimorphismpolynomialproofwikiring-theory
Over an infinite integral domain, the evaluation map from polynomials to polynomial functions is injective.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.RingTheory.Polynomial.Basic
Formal statement
theorem Epimorphism_from_Polynomial_Forms_to_Polynomial_Functions {D : Type _} [CommRing D] [IsDomain D] [Infinite D] : Function.Injective (Polynomial.eval : D → Polynomial D → D) := by sorrySource