Theory Poly_Divisibility

section ‹The polynomial ring over a field is a Euclidean domain›

theory Poly_Divisibility
  imports Poly_Ring Divisibility_Theory Poly_Ideal
begin

text ‹Over a field ‹F›, the polynomial ring ‹F[X]› is a Euclidean domain, with the polynomial
  degree as Euclidean function: this is exactly the division algorithm of
  ‹Poly_Ring› (@{thm [source] Field.poly_divide}) packaged into the abstract
  @{locale Euclidean_Domain} of ‹Divisibility_Theory›.  The interpretation is
  the bridge that endows ‹F[X]› --- for free --- with the whole divisibility tower: it is a
  principal ideal domain and a factorial (unique factorization) domain, in which irreducible
  polynomials are prime and factorizations into irreducibles exist and are unique up to the number
  of factors.›

context Field
begin

text ‹The carrier-set polynomial ring satisfies the abstract Euclidean-domain interface.  This
  named theorem keeps the division-algorithm proof reusable by the exported sublocale below.›
theorem poly_euclidean_domain:
  "Euclidean_Domain poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P degree"
proof -
  show "Euclidean_Domain poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P degree"
  proof (rule Euclidean_Domain.intro)
    show "integral_domain poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P"
      by (rule poly_integral_domain)
  next
    show "Euclidean_Domain_axioms poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P degree"
    proof
      fix a b assume a: "a ∈ poly_carrier" and b: "b ∈ poly_carrier"
        and anz: "a ≠ 𝟬⇩P" and bnz: "b ≠ 𝟬⇩P"
      show "∃q∈poly_carrier. ∃r∈poly_carrier.
              a = (b ⊗⇩P q) ⊕⇩P r ∧ (r = 𝟬⇩P ∨ degree r < degree b)"
        using poly_divide[OF a b bnz] by blast
    qed
  qed
qed

end

sublocale Field ⊆ FX: Euclidean_Domain
  poly_carrier "(⊕⇩P)" "(⊗⇩P)" "𝟬⇩P" "𝟭⇩P" degree
proof -
  show "Euclidean_Domain poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P degree"
    by (rule poly_euclidean_domain)
qed

context Field
begin

text ‹Consequences, transported from the abstract tower.  Every nonzero non-unit polynomial factors
  into irreducibles (@{thm [source] FX.factorization_exists}), an irreducible polynomial is prime
  (@{thm [source] FX.irreducible_imp_prime}), and any two prime factorizations of associated
  polynomials have the same length (@{thm [source] FX.prime_factorization_length_unique}).›

theorem poly_factorization_exists:
  "⟦ p ∈ poly_carrier; p ≠ 𝟬⇩P; ¬ FX.is_unit p ⟧ ⟹ ∃fs. FX.factorization fs p"
  by (rule FX.factorization_exists)

theorem poly_irreducible_imp_prime:
  "FX.irreducible_elem p ⟹ FX.prime_elem p"
  by (rule FX.irreducible_imp_prime)

end


text ‹
  ‹Poly_Divisibility› interprets the carrier-set polynomial ring as an
  abstract Euclidean domain, while ‹Poly_Ideal› exposes the same multiples
  through @{const Field.poly_dvd} and @{const Field.poly_pideal}.  The two interfaces are
  intentionally kept in their original theories so that each remains independently usable.  This
  theory is the explicit seam between them.
›

context Field
begin

text ‹
  The concrete polynomial divisibility relation and the abstract relation differ only by the
  orientation of the product.  Commutativity of the polynomial ring supplies the bridge.
›
lemma FX_divides_iff_poly_dvd:
  assumes d: "d ∈ poly_carrier"
  shows "FX.divides d x ⟷ poly_dvd d x"
proof
  assume dvd: "FX.divides d x"
  obtain q where q: "q ∈ poly_carrier" and xeq: "x = d ⊗⇩P q"
    using FX.dividesE[OF dvd] by blast
  have "x = q ⊗⇩P d"
  proof -
    have "d ⊗⇩P q = q ⊗⇩P d" using d q by (rule poly_mult_comm)
    then show ?thesis using xeq by simp
  qed
  then show "poly_dvd d x"
    unfolding poly_dvd_def using q by blast
next
  assume dvd: "poly_dvd d x"
  obtain q where q: "q ∈ poly_carrier" and xeq: "x = q ⊗⇩P d"
    using dvd unfolding poly_dvd_def by blast
  have "x = d ⊗⇩P q"
  proof -
    have "q ⊗⇩P d = d ⊗⇩P q" using q d by (rule poly_mult_comm)
    then show ?thesis using xeq by simp
  qed
  show "FX.divides d x"
  proof (rule FX.dividesI)
    show "q ∈ poly_carrier" using q .
    show "x = d ⊗⇩P q" using ‹x = d ⊗⇩P q› .
  qed
qed

text ‹
  The concrete principal ideal and the abstract divisibility relation now have a common
  polynomial-level formulation.
›
lemma FX_divides_iff_mem_poly_pideal:
  assumes d: "d ∈ poly_carrier"
  shows "FX.divides d x ⟷ x ∈ poly_pideal d"
  using FX_divides_iff_poly_dvd[OF d] poly_dvd_iff_mem_pideal by blast

lemma poly_dvd_iff_mem_FX_principal:
  assumes d: "d ∈ poly_carrier" and x: "x ∈ poly_carrier"
  shows "poly_dvd d x ⟷ x ∈ FX.principal_ideal d"
  using FX_divides_iff_poly_dvd[OF d] FX.divides_iff_mem_principal[OF d x] by blast

lemma FX_divides_iff_pmod_zero:
  assumes d: "d ∈ poly_carrier" and dnz: "d ≠ 𝟬⇩P"
    and x: "x ∈ poly_carrier"
  shows "FX.divides d x ⟷ pmod x d = 𝟬⇩P"
  using FX_divides_iff_poly_dvd[OF d] poly_dvd_iff_pmod_zero[OF d dnz x] by blast


subsection ‹Units and irreducibility across the seam›

text ‹
  The same seam again one notion up.  @{const poly_unit} spells out invertibility in the polynomial
  ring directly, while @{term FX.is_unit} is the abstract @{const Monoid.invertible} at that ring.
  ∗‹They are not quite the same predicate›: @{const Monoid.invertible} does not require its argument to
  lie in the carrier, whereas @{const poly_unit} does, so the two agree only on @{const poly_carrier}.
  That is enough for the notion actually wanted, because @{const poly_irreducible} and
  @{term FX.irreducible_elem} both demand carrier membership outright and apply their unit test only
  to carrier elements.  Their agreement is what lets a factor produced by
  @{thm [source] poly_factorization_exists} be fed to @{thm [source] poly_quotient_field}.
›

lemma FX_is_unit_iff_poly_unit:
  assumes p: "p ∈ poly_carrier" shows "FX.is_unit p ⟷ poly_unit p"
proof
  assume "FX.is_unit p"
  then obtain q where "q ∈ poly_carrier" and "p ⊗⇩P q = 𝟭⇩P" and "q ⊗⇩P p = 𝟭⇩P" by blast
  with p show "poly_unit p" by (rule poly_unitI)
next
  assume "poly_unit p"
  then obtain q where q: "q ∈ poly_carrier" and pq: "p ⊗⇩P q = 𝟭⇩P" and qp: "q ⊗⇩P p = 𝟭⇩P"
    unfolding poly_unit_def by blast
  show "FX.is_unit p" by (rule FX.is_unitI [OF pq qp q])
qed

lemma FX_irreducible_iff_poly_irreducible:
  "FX.irreducible_elem p ⟷ poly_irreducible p"
  unfolding FX.irreducible_elem_def poly_irreducible_def
  by (auto simp: FX_is_unit_iff_poly_unit)

text ‹
  Every polynomial that is neither zero nor a unit has an irreducible factor: factor it and take the
  head of the list, which is nonempty because the empty product is @{term "𝟭⇩P"}.  This is the form
  in which the adjunction of a root consumes factorization --- a root of an irreducible factor of
  @{term p} is a root of @{term p} --- and it is stated with @{const poly_irreducible} so that
  @{thm [source] poly_quotient_field} applies directly.
›
theorem exists_poly_irreducible_factor:
  assumes p: "p ∈ poly_carrier" and pnz: "p ≠ 𝟬⇩P" and pnu: "¬ poly_unit p"
  obtains q where "poly_irreducible q" and "poly_dvd q p"
proof -
  have "¬ FX.is_unit p" using pnu by (simp add: FX_is_unit_iff_poly_unit [OF p])
  then obtain fs where fs: "FX.factorization fs p"
    using poly_factorization_exists [OF p pnz] by blast
  have prod: "FX.list_prod fs = p" by (rule FX.factorization_prod [OF fs])
  have "fs ≠ []"
  proof
    assume "fs = []"
    with prod have peq: "p = 𝟭⇩P" by simp
    have "poly_unit 𝟭⇩P"
      by (rule poly_unitI [OF poly_one_closed poly_one_closed])
         (simp_all add: poly_mult_one_left poly_one_closed)
    with peq pnu show False by simp
  qed
  then obtain f gs where feq: "fs = f # gs" by (cases fs) auto
  have irr: "FX.irreducible_elem f" using fs feq by (simp add: FX.factorization_irreducible)
  have fc: "f ∈ poly_carrier" using irr by (rule FX.irreducible_elemD(1))
  have gsR: "set gs ⊆ poly_carrier" using FX.factorization_set_R [OF fs] feq by simp
  have "p = f ⊗⇩P FX.list_prod gs" using prod feq by simp
  then have "poly_dvd f p"
    using FX.list_prod_closed [OF gsR] fc by (auto simp: poly_dvd_def poly_mult_comm)
  with irr show thesis
    using that FX_irreducible_iff_poly_irreducible by blast
qed

text ‹Each member of a list divides the product of the list.  Needed to feed a single irreducible
  factor of a factorisation to the adjunction of a root.›
lemma poly_dvd_poly_prod:
  assumes fs: "⋀g. g ∈ set fs ⟹ g ∈ poly_carrier" and f: "f ∈ set fs"
  shows "poly_dvd f (poly_prod fs)"
  using fs f
proof (induct fs)
  case (Cons g gs)
  have gc: "g ∈ poly_carrier" and gsc: "⋀h. h ∈ set gs ⟹ h ∈ poly_carrier"
    using Cons.prems(1) by auto
  have Pgs: "poly_prod gs ∈ poly_carrier" by (rule poly_prod_closed [OF gsc])
  show ?case
  proof (cases "f = g")
    case True
    have "poly_prod (g # gs) = poly_prod gs ⊗⇩P g"
      using poly_mult_comm [OF gc Pgs] by simp
    then show ?thesis unfolding poly_dvd_def using True Pgs by blast
  next
    case False
    then have "f ∈ set gs" using Cons.prems(2) by simp
    then obtain q where q: "q ∈ poly_carrier" and eq: "poly_prod gs = q ⊗⇩P f"
      using Cons.hyps [OF gsc] unfolding poly_dvd_def by blast
    have fc: "f ∈ poly_carrier" using ‹f ∈ set gs› by (rule gsc)
    have "poly_prod (g # gs) = (g ⊗⇩P q) ⊗⇩P f"
      using eq poly_mult_assoc [OF gc q fc] by simp
    then show ?thesis unfolding poly_dvd_def using gc q by (blast intro: poly_mult_closed)
  qed
qed simp

subsection ‹The field of remainders modulo an irreducible polynomial›

text ‹
  Kronecker's theorem in ∗‹normal-form› presentation: rather than the cosets of ‹(p)›, take the
  polynomials of degree below @{term p}, with addition unchanged and multiplication followed by
  reduction.  This is the same field as @{thm [source] poly_quotient_field} exhibits, but its carrier
  is a set of polynomials rather than a set of cosets, so it stays inside the coefficient type.  That
  is what a construction adjoining roots inside a fixed ambient type needs, and it is also the form
  in which one computes.

  Invertibility is the only substantial part, and it does not need gcds: a nonzero remainder is not a
  multiple of @{term p}, so it lies outside the maximal ideal ‹(p)›, and extending that ideal by it
  gives the whole ring --- which is to say @{term "𝟭⇩P"} is a combination @{term "m ⊕⇩P r ⊗⇩P S"} with
  @{term m} a multiple of @{term p}.  Reducing that equation is exactly the inverse.
›
theorem remainder_field:
  assumes irr: "poly_irreducible p"
  shows "Field (low_poly (degree p)) (⊕⇩P) (λS T. pmod (S ⊗⇩P T) p) 𝟬⇩P 𝟭⇩P"
proof -
  have p: "p ∈ poly_carrier" using irr by (rule poly_irreducibleD_carrier)
  have pnz: "p ≠ 𝟬⇩P" using irr by (rule poly_irreducibleD_nonzero)
  have dpos: "0 < degree p" using irr by (rule poly_irreducible_degree_pos)
  define K where "K = low_poly (degree p)"
  define mult where "mult = (λS T. pmod (S ⊗⇩P T) p)"
  ― ‹Basic facts about the carrier.›
  have Kc: "S ∈ poly_carrier" if "S ∈ K" for S
    using that unfolding K_def by (rule low_poly_closed)
  have Ksmall: "pmod S p = S" if "S ∈ K" for S
    using that low_poly_iff_degree [OF Kc [OF that]] pmod_small [OF p pnz Kc [OF that]]
    unfolding K_def by blast
  have Kadd: "S ⊕⇩P T ∈ K" if "S ∈ K" "T ∈ K" for S T
    using that unfolding K_def by (rule low_poly_add_closed)
  have Kneg: "⊖⇩P S ∈ K" if "S ∈ K" for S
    using that unfolding K_def by (rule low_poly_neg_closed)
  have Kzero: "𝟬⇩P ∈ K" unfolding K_def by (rule low_poly_zero)
  have Kone: "𝟭⇩P ∈ K" unfolding K_def using dpos by (rule low_poly_one)
  have Kmult: "mult S T ∈ K" if "S ∈ K" "T ∈ K" for S T
    unfolding mult_def K_def
    using poly_mult_closed [OF Kc [OF that(1)] Kc [OF that(2)]] p pnz by (rule pmod_low_poly)
  ― ‹Reduction is a homomorphism, so it carries the ring laws over from @{text "F[X]"}.›
  have reduce: "pmod (S ⊗⇩P T) p = mult S T" for S T unfolding mult_def by rule
  have mult_assoc: "mult (mult S T) U = mult S (mult T U)" if K: "S ∈ K" "T ∈ K" "U ∈ K" for S T U
  proof -
    have c: "S ∈ poly_carrier" "T ∈ poly_carrier" "U ∈ poly_carrier"
      using K by (blast intro: Kc)+
    have "mult (mult S T) U = pmod (pmod (S ⊗⇩P T) p ⊗⇩P pmod U p) p"
      unfolding mult_def using Ksmall [OF K(3)] by simp
    also have "… = pmod ((S ⊗⇩P T) ⊗⇩P U) p"
      by (rule pmod_mult [OF poly_mult_closed [OF c(1) c(2)] c(3) p pnz, symmetric])
    also have "… = pmod (S ⊗⇩P (T ⊗⇩P U)) p" using poly_mult_assoc [OF c] by simp
    also have "… = pmod (pmod S p ⊗⇩P pmod (T ⊗⇩P U) p) p"
      by (rule pmod_mult [OF c(1) poly_mult_closed [OF c(2) c(3)] p pnz])
    also have "… = mult S (mult T U)"
      unfolding mult_def using Ksmall [OF K(1)] by simp
    finally show ?thesis .
  qed
  have mult_comm: "mult S T = mult T S" if "S ∈ K" "T ∈ K" for S T
    unfolding mult_def using poly_mult_comm [OF Kc [OF that(1)] Kc [OF that(2)]] by simp
  have mult_one: "mult 𝟭⇩P S = S" if "S ∈ K" for S
    unfolding mult_def
    using poly_mult_one_left [OF Kc [OF that]] Ksmall [OF that] by simp
  have distrib: "mult S (T ⊕⇩P U) = mult S T ⊕⇩P mult S U" if K: "S ∈ K" "T ∈ K" "U ∈ K" for S T U
  proof -
    have c: "S ∈ poly_carrier" "T ∈ poly_carrier" "U ∈ poly_carrier"
      using K by (blast intro: Kc)+
    have "mult S (T ⊕⇩P U) = pmod ((S ⊗⇩P T) ⊕⇩P (S ⊗⇩P U)) p"
      unfolding mult_def using poly_mult_add_distrib_left [OF c] by simp
    also have "… = pmod (S ⊗⇩P T) p ⊕⇩P pmod (S ⊗⇩P U) p"
      by (rule pmod_add [OF poly_mult_closed [OF c(1) c(2)] poly_mult_closed [OF c(1) c(3)] p pnz])
    finally show ?thesis unfolding mult_def .
  qed
  ― ‹A nonzero remainder is invertible: it escapes the maximal ideal ‹(p)›.›
  have inverse: "∃T ∈ K. mult S T = 𝟭⇩P" if S: "S ∈ K" and Snz: "S ≠ 𝟬⇩P" for S
  proof -
    interpret I: ideal_in_comm_ring "poly_pideal p" poly_carrier "(⊕⇩P)" "(⊗⇩P)" "𝟬⇩P" "𝟭⇩P"
      by (rule poly_pideal_in_comm_ring [OF p])
    have Sc: "S ∈ poly_carrier" using S by (rule Kc)
    have "pmod S p ≠ 𝟬⇩P" using Ksmall [OF S] Snz by simp
    then have SnotI: "S ∉ poly_pideal p" using poly_pideal_iff_pmod [OF p pnz Sc] by simp
    have "𝟭⇩P ∈ I.ext_ideal S"
      using I.maximal_ext_ideal_eq_whole [OF poly_irreducible_maximal [OF irr] Sc SnotI]
            poly_one_closed by simp
    then obtain m r where m: "m ∈ poly_pideal p" and r: "r ∈ poly_carrier"
        and one: "𝟭⇩P = m ⊕⇩P (r ⊗⇩P S)"
      unfolding I.ext_ideal_def by blast
    have mc: "m ∈ poly_carrier"
    proof -
      obtain u where u: "u ∈ poly_carrier" and meq: "m = u ⊗⇩P p"
        using m unfolding poly_pideal_def by blast
      show ?thesis using meq poly_mult_closed [OF u p] by simp
    qed
    have mz: "pmod m p = 𝟬⇩P" using m poly_pideal_iff_pmod [OF p pnz mc] by simp
    ― ‹Reduce the combination: the multiple of @{term p} disappears.›
    have "𝟭⇩P = pmod 𝟭⇩P p" using pmod_small [OF p pnz poly_one_closed] Kone Ksmall by simp
    also have "… = pmod m p ⊕⇩P pmod (r ⊗⇩P S) p"
      using one pmod_add [OF mc poly_mult_closed [OF r Sc] p pnz] by simp
    also have "… = pmod (r ⊗⇩P S) p"
      using mz pmod_closed [OF poly_mult_closed [OF r Sc] p pnz] by (simp add: poly_add_zero)
    also have "… = pmod (pmod r p ⊗⇩P pmod S p) p"
      by (rule pmod_mult [OF r Sc p pnz])
    also have "… = mult S (pmod r p)"
      unfolding mult_def using Ksmall [OF S] poly_mult_comm [OF Sc pmod_closed [OF r p pnz]] by simp
    finally have "mult S (pmod r p) = 𝟭⇩P" by simp
    moreover have "pmod r p ∈ K" unfolding K_def using r p pnz by (rule pmod_low_poly)
    ultimately show ?thesis by blast
  qed
  ― ‹Assemble.›
  have grp: "Group K (⊕⇩P) 𝟬⇩P"
  proof (rule GroupI)
    show "⋀x y. ⟦ x ∈ K; y ∈ K ⟧ ⟹ x ⊕⇩P y ∈ K" by (rule Kadd)
    show "𝟬⇩P ∈ K" by (rule Kzero)
    show "⋀x y z. ⟦ x ∈ K; y ∈ K; z ∈ K ⟧ ⟹ (x ⊕⇩P y) ⊕⇩P z = x ⊕⇩P (y ⊕⇩P z)"
      using Kc by (blast intro: poly_add_assoc)
    show "⋀x. x ∈ K ⟹ 𝟬⇩P ⊕⇩P x = x" using Kc by (blast intro: poly_add_zero)
    show "⋀x. x ∈ K ⟹ x ⊕⇩P 𝟬⇩P = x"
      using Kc poly_add_comm poly_zero_closed by (metis poly_add_zero)
    show "⋀x. x ∈ K ⟹ ∃y ∈ K. x ⊕⇩P y = 𝟬⇩P ∧ y ⊕⇩P x = 𝟬⇩P"
      using Kneg Kc poly_add_neg poly_add_neg_right by blast
  qed
  interpret A: Group K "(⊕⇩P)" "𝟬⇩P" by (rule grp)
  interpret A: Abelian_Group K "(⊕⇩P)" "𝟬⇩P"
    by unfold_locales (use Kc poly_add_comm in blast)
  have mult_one': "mult S 𝟭⇩P = S" if S: "S ∈ K" for S
  proof -
    have "mult S 𝟭⇩P = mult 𝟭⇩P S" by (rule mult_comm [OF S Kone])
    also have "… = S" by (rule mult_one [OF S])
    finally show ?thesis .
  qed
  interpret M: commutative_monoid K mult "𝟭⇩P"
  proof unfold_locales
    show "⋀a b. ⟦ a ∈ K; b ∈ K ⟧ ⟹ mult a b ∈ K" by (rule Kmult)
    show "𝟭⇩P ∈ K" by (rule Kone)
    show "⋀a b c. ⟦ a ∈ K; b ∈ K; c ∈ K ⟧
                   ⟹ mult (mult a b) c = mult a (mult b c)" by (rule mult_assoc)
    show "⋀a. a ∈ K ⟹ mult 𝟭⇩P a = a" by (rule mult_one)
    show "⋀a. a ∈ K ⟹ mult a 𝟭⇩P = a" by (rule mult_one')
    show "⋀x y. ⟦ x ∈ K; y ∈ K ⟧ ⟹ mult x y = mult y x" by (rule mult_comm)
  qed
  show ?thesis
    unfolding sym [OF K_def] sym [OF mult_def]
  proof unfold_locales
    show "⋀x y z. ⟦ x ∈ K; y ∈ K; z ∈ K ⟧
                   ⟹ mult x (y ⊕⇩P z) = mult x y ⊕⇩P mult x z" by (rule distrib)
    show "⋀x y z. ⟦ x ∈ K; y ∈ K; z ∈ K ⟧
                   ⟹ mult (y ⊕⇩P z) x = mult y x ⊕⇩P mult z x"
    proof -
      fix x y z assume K: "x ∈ K" "y ∈ K" "z ∈ K"
      have "mult (y ⊕⇩P z) x = mult x (y ⊕⇩P z)"
        by (rule mult_comm [OF Kadd [OF K(2) K(3)] K(1)])
      also have "… = mult x y ⊕⇩P mult x z" by (rule distrib [OF K])
      also have "… = mult y x ⊕⇩P mult z x"
        using mult_comm [OF K(1) K(2)] mult_comm [OF K(1) K(3)] by simp
      finally show "mult (y ⊕⇩P z) x = mult y x ⊕⇩P mult z x" .
    qed
    show "𝟭⇩P ≠ 𝟬⇩P" by (metis nontrivial poly_one_def poly_zero_def)
    show "⋀x. ⟦ x ∈ K; x ≠ 𝟬⇩P ⟧ ⟹ M.invertible x"
    proof -
      fix x assume x: "x ∈ K" and xnz: "x ≠ 𝟬⇩P"
      obtain T where T: "T ∈ K" and xT: "mult x T = 𝟭⇩P" using inverse [OF x xnz] by blast
      have "mult T x = 𝟭⇩P" using xT mult_comm [OF x T] by simp
      with xT T show "M.invertible x" by (blast intro: M.invertibleI)
    qed
  qed
qed

text ‹∗‹The adjoined root really is a root.›  Evaluating in the field of remainders, at the variable
  and with the coefficients embedded as constants, reduces the polynomial modulo the modulus.  So the
  class of @{term q} is the value of @{term q} at the variable, and when the modulus divides @{term q}
  that value is zero.

  Reduction is a ring homomorphism from @{text "F[X]"} onto the remainders, by
  @{thm [source] pmod_add} and @{thm [source] pmod_mult}, and it fixes the variable and the constants
  because those are already of low degree --- which is where @{term "2 ≤ degree p"} is needed.  So
  @{thm [source] eval_hom} applies, and the source evaluation is the polynomial itself by
  @{thm [source] eval_const_lift_at_var}.›
theorem eval_remainder_at_var:
  assumes irr: "poly_irreducible p" and d2: "2 ≤ degree p" and q: "q ∈ poly_carrier"
  shows "Ring.eval (low_poly (degree p)) (⊕⇩P) (λS T. pmod (S ⊗⇩P T) p)
           𝟬⇩P 𝟭⇩P X⇩P (λk. poly_const (q k)) = pmod q p"
proof -
  have pc: "p ∈ poly_carrier" using irr by (rule poly_irreducibleD_carrier)
  have pnz: "p ≠ 𝟬⇩P" using irr by (rule poly_irreducibleD_nonzero)
  have RB: "Ring (low_poly (degree p)) (⊕⇩P) (λS T. pmod (S ⊗⇩P T) p) 𝟬⇩P 𝟭⇩P"
    using remainder_field [OF irr] by (simp add: Field_def commutative_ring_def)
  have coeffR: "q k ∈ R" for k using q by (rule poly_carrier_coeff_closed)
  have constc: "poly_const (q k) ∈ poly_carrier" for k using coeffR by (rule poly_const_closed)
  ― ‹Reduction fixes the constants and the variable, both being of low degree.›
  have fix_const: "pmod (poly_const (q k)) p = poly_const (q k)" for k
  proof (rule pmod_small [OF pc pnz constc])
    have "degree (poly_const (q k)) = 0" using degree_const_le by (simp add: le_zero_eq)
    then show "poly_const (q k) = 𝟬⇩P ∨ degree (poly_const (q k)) < degree p"
      using d2 by simp
  qed
  have fix_var: "pmod X⇩P p = X⇩P"
    by (rule pmod_small [OF pc pnz var_closed])
       (use d2 degree_var [OF nontrivial] in simp)
  have "Ring.eval (low_poly (degree p)) (⊕⇩P) (λS T. pmod (S ⊗⇩P T) p)
          𝟬⇩P 𝟭⇩P (pmod X⇩P p) (λk. pmod (poly_const (q k)) p)
        = pmod (Ring.eval poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P X⇩P (λk. poly_const (q k))) p"
  proof (rule eval_hom [OF poly_ring RB])
    show "⋀S. S ∈ poly_carrier ⟹ pmod S p ∈ low_poly (degree p)"
      using pc pnz by (blast intro: pmod_low_poly)
    show "pmod 𝟬⇩P p = 𝟬⇩P" by (rule pmod_small [OF pc pnz poly_zero_closed]) simp
    show "pmod 𝟭⇩P p = 𝟭⇩P"
      by (rule pmod_small [OF pc pnz poly_one_closed]) (use d2 degree_one in simp)
    show "⋀S T. ⟦ S ∈ poly_carrier; T ∈ poly_carrier ⟧
                  ⟹ pmod (S ⊕⇩P T) p = pmod S p ⊕⇩P pmod T p"
      using pc pnz by (blast intro: pmod_add)
    show "⋀S T. ⟦ S ∈ poly_carrier; T ∈ poly_carrier ⟧
                  ⟹ pmod (S ⊗⇩P T) p = pmod (pmod S p ⊗⇩P pmod T p) p"
      using pc pnz by (blast intro: pmod_mult)
    show "X⇩P ∈ poly_carrier" by (rule var_closed)
    show "⋀k. poly_const (q k) ∈ poly_carrier" by (rule constc)
    show "Ring.degree 𝟬⇩P (λk. pmod (poly_const (q k)) p)
          = Ring.degree 𝟬⇩P (λk. poly_const (q k))"
      using fix_const by simp
  qed
  then show ?thesis
    using fix_var fix_const eval_const_lift_at_var [OF q] by simp
qed

end

end