The coefficient of highest possible degree on an affine line depends only on the top homogeneous component and the direction, not the base point.

theorem CCDN.polynomial_affine_natDegree_le {R : Type u_1} [CommRing R] (a b : R) : (Polynomial.C a + Polynomial.C b * Polynomial.X).natDegree ≤ 1

The affine polynomial C a + C b * X has degree at most 1.

noncomputable def CCDN.affineLinePolynomial {R : Type u_1} {σ : Type u_2} [CommRing R] (a b : σ → R) : MvPolynomial σ R →+* Polynomial R

Restriction to the affine line a+t*b.

Equations

• CCDN.affineLinePolynomial a b = MvPolynomial.eval₂Hom Polynomial.C fun (i : σ) => Polynomial.C (a i) + Polynomial.C (b i) * Polynomial.X

theorem CCDN.affineLinePolynomial_top_coefficient {R : Type u_1} {σ : Type u_2} [CommRing R] (a b : σ → R) (f : MvPolynomial σ R) (d : ℕ) (hd : f.totalDegree ≤ d) : ((affineLinePolynomial a b) f).coeff d = (MvPolynomial.eval b) ((MvPolynomial.homogeneousComponent d) f)

At any degree at least the total degree, the affine-line coefficient equals the corresponding homogeneous component evaluated on its direction.