Specializing a polynomial at a parameter
DefinitionEsgk_IrreduciblePlaneAffineNormalizationNonsingularLiftalgebracommutative-algebrapolynomials
This evaluates the coefficients of a generic polynomial at a specified parameter into a target ring, producing the specialized polynomial.
Definition code
-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_LeanFormalizations_PachDeZeeuw_Bezout
import Mathlib
/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/
noncomputable section
namespace Esgk
open PachDeZeeuw.Algebraic
namespace IrreduciblePlanePolynomial
open MvPolynomial
def specializeAt {R : Type*} [CommRing R] {σ : Type*} [DecidableEq σ]
(i : σ) (c : R) : MvPolynomial σ R →+* MvPolynomial σ R :=
MvPolynomial.eval₂Hom (C : R →+* MvPolynomial σ R)
(fun k => if k = i then C c else X k)
end IrreduciblePlanePolynomial
end Esgk