Exact total degree and coefficient extension for the explicit grid equation.

theorem CCDN.gridEisensteinPolynomial_totalDegree {K : Type u_1} [Field K] (V : Polynomial K) (k : ℕ) (hm : V.Monic) (hd : 0 < V.natDegree) (h0 : V.coeff 0 ≠ 0) (hk : 2 ≤ k) (hs : V.natDegree ≤ k + 1) : bivariateTotalDegree (gridEisensteinPolynomial V k) = V.natDegree + k

If s≤k+1, the explicit equation has exact total degree s+k.

theorem CCDN.gridEisensteinPolynomial_map_irreducible {K : Type u_1} {L : Type u_2} [Field K] [Field L] (φ : K →+* L) (V : Polynomial K) (k : ℕ) (hm : V.Monic) (hd : 0 < V.natDegree) (h0 : V.coeff 0 ≠ 0) (hk : 2 ≤ k) : Irreducible ((bivariateMap φ) (gridEisensteinPolynomial V k))

Absolute irreducibility is stable under every field extension here because Eisenstein applies to the same explicit equation after coefficient extension.