@[reducible, inline]

abbrev Polynomials.IsPrimitivePolynomial {R : Type u_1} [CommSemiring R] (p : Polynomial R) : Prop

instance Polynomials.polynomialUFD (F : Type u_1) [Field F] : UniqueFactorizationMonoid (Polynomial F)

noncomputable def Polynomials.evalRingHom (R : Type u_1) [CommRing R] (α : R) : Polynomial R →+* R

theorem Polynomials.polynomial_mapping_property {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) {σ : Type u_3} (α : σ → S) : ∃! ψ : MvPolynomial σ R →+* S, (∀ (r : R), ψ (MvPolynomial.C r) = φ r) ∧ ∀ (i : σ), ψ (MvPolynomial.X i) = α i