Theory HOL-Algebra.Polynomial_Divisibility

(*  Title:      HOL/Algebra/Polynomial_Divisibility.thy
    Author:     Paulo Emílio de Vilhena
*)

theory Polynomial_Divisibility
  imports Polynomials Embedded_Algebras "HOL-Library.Multiset"
    
begin

section ‹Divisibility of Polynomials›

subsection ‹Definitions›

abbreviation poly_ring :: "_  ('a  list) ring"
  where "poly_ring R  univ_poly R (carrier R)"

abbreviation pirreducible :: "_  'a set  'a list  bool" (pirreducibleı›)
  where "pirreducibleRK p  ring_irreducible(univ_poly R K)p"

abbreviation pprime :: "_  'a set  'a list  bool" (pprimeı›)
  where "pprimeRK p  ring_prime(univ_poly R K)p"

definition pdivides :: "_  'a list  'a list  bool" (infix pdividesı› 65)
  where "p pdividesRq = p divides(univ_poly R (carrier R))q"

definition rupture :: "_  'a set  'a list  (('a list) set) ring" (Ruptı›)
  where "RuptRK p = (K[X]R) Quot (PIdlK[X]R⇙⇙ p)"

abbreviation (in ring) rupture_surj :: "'a set  'a list  'a list  ('a list) set"
  where "rupture_surj K p  (λq. (PIdlK[X]p) +>K[X]q)"


subsection ‹Basic Properties›

lemma (in ring) carrier_polynomial_shell [intro]:
  assumes "subring K R" and "p  carrier (K[X])" shows "p  carrier (poly_ring R)"
  using carrier_polynomial[OF assms(1), of p] assms(2) unfolding sym[OF univ_poly_carrier] by simp

lemma (in domain) pdivides_zero:
  assumes "subring K R" and "p  carrier (K[X])" shows "p pdivides []"
  using ring.divides_zero[OF univ_poly_is_ring[OF carrier_is_subring]
         carrier_polynomial_shell[OF assms]]
  unfolding univ_poly_zero pdivides_def .

lemma (in domain) zero_pdivides_zero: "[] pdivides []"
  using pdivides_zero[OF carrier_is_subring] univ_poly_carrier by blast

lemma (in domain) zero_pdivides:
  shows "[] pdivides p  p = []"
  using ring.zero_divides[OF univ_poly_is_ring[OF carrier_is_subring]]
  unfolding univ_poly_zero pdivides_def .

lemma (in domain) pprime_iff_pirreducible:
  assumes "subfield K R" and "p  carrier (K[X])"
  shows "pprime K p  pirreducible K p"
  using principal_domain.primeness_condition[OF univ_poly_is_principal] assms by simp

lemma (in domain) pirreducibleE:
  assumes "subring K R" "p  carrier (K[X])" "pirreducible K p"
  shows "p  []" "p  Units (K[X])"
    and "q r.  q  carrier (K[X]); r  carrier (K[X]) 
                 p = q K[X]r  q  Units (K[X])  r  Units (K[X])"
  using domain.ring_irreducibleE[OF univ_poly_is_domain[OF assms(1)] _ assms(3)] assms(2)
  by (auto simp add: univ_poly_zero)

lemma (in domain) pirreducibleI:
  assumes "subring K R" "p  carrier (K[X])" "p  []" "p  Units (K[X])"
    and "q r.  q  carrier (K[X]); r  carrier (K[X]) 
                 p = q K[X]r  q  Units (K[X])  r  Units (K[X])"
  shows "pirreducible K p"
  using domain.ring_irreducibleI[OF univ_poly_is_domain[OF assms(1)] _ assms(4)] assms(2-3,5)
  by (auto simp add: univ_poly_zero)

lemma (in domain) univ_poly_carrier_units_incl:
  shows "Units ((carrier R) [X])  { [ k ] | k. k  carrier R - { 𝟬 } }"
proof
  fix p assume "p  Units ((carrier R) [X])"
  then obtain q
    where p: "polynomial (carrier R) p" and q: "polynomial (carrier R) q" and pq: "poly_mult p q = [ 𝟭 ]"
    unfolding Units_def univ_poly_def by auto
  hence not_nil: "p  []" and "q  []"
    using poly_mult_integral[OF carrier_is_subring p q] poly_mult_zero[OF polynomial_incl[OF p]] by auto
  hence "degree p = 0"
    using poly_mult_degree_eq[OF carrier_is_subring p q] unfolding pq by simp
  hence "length p = 1"
    using not_nil by (metis One_nat_def Suc_pred length_greater_0_conv)
  then obtain k where k: "p = [ k ]"
    by (metis One_nat_def length_0_conv length_Suc_conv)
  hence "k  carrier R - { 𝟬 }"
    using p unfolding polynomial_def by auto 
  thus "p  { [ k ] | k. k  carrier R - { 𝟬 } }"
    unfolding k by blast
qed

lemma (in field) univ_poly_carrier_units:
  "Units ((carrier R) [X]) = { [ k ] | k. k  carrier R - { 𝟬 } }"
proof
  show "Units ((carrier R) [X])  { [ k ] | k. k  carrier R - { 𝟬 } }"
    using univ_poly_carrier_units_incl by simp
next
  show "{ [ k ] | k. k  carrier R - { 𝟬 } }  Units ((carrier R) [X])"
  proof (auto)
    fix k assume k: "k  carrier R" "k  𝟬"
    hence inv_k: "inv k  carrier R" "inv k  𝟬" and "k  inv k = 𝟭" "inv k  k = 𝟭"
      using subfield_m_inv[OF carrier_is_subfield, of k] by auto
    hence "poly_mult [ k ] [ inv k ] = [ 𝟭 ]" and "poly_mult [ inv k ] [ k ] = [ 𝟭 ]"
      by (auto simp add: k)
    moreover have "polynomial (carrier R) [ k ]" and "polynomial (carrier R) [ inv k ]"
      using const_is_polynomial k inv_k by auto
    ultimately show "[ k ]  Units ((carrier R) [X])"
      unfolding Units_def univ_poly_def by (auto simp del: poly_mult.simps)
  qed
qed

lemma (in domain) univ_poly_units_incl:
  assumes "subring K R" shows "Units (K[X])  { [ k ] | k. k  K - { 𝟬 } }"
  using domain.univ_poly_carrier_units_incl[OF subring_is_domain[OF assms]]
        univ_poly_consistent[OF assms] by auto

lemma (in ring) univ_poly_units:
  assumes "subfield K R" shows "Units (K[X]) = { [ k ] | k. k  K - { 𝟬 } }"
  using field.univ_poly_carrier_units[OF subfield_iff(2)[OF assms]]
        univ_poly_consistent[OF subfieldE(1)[OF assms]] by auto

lemma (in domain) univ_poly_units':
  assumes "subfield K R" shows "p  Units (K[X])  p  carrier (K[X])  p  []  degree p = 0"
  unfolding univ_poly_units[OF assms] sym[OF univ_poly_carrier] polynomial_def
  by (auto, metis hd_in_set le_0_eq le_Suc_eq length_0_conv length_Suc_conv list.sel(1) subsetD)

corollary (in domain) rupture_one_not_zero:
  assumes "subfield K R" and "p  carrier (K[X])" and "degree p > 0"
  shows "𝟭Rupt K p 𝟬Rupt K p⇙"
proof (rule ccontr)
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] . 

  assume "¬ 𝟭Rupt K p 𝟬Rupt K p⇙"
  then have "PIdlK[X]p +>K[X]𝟭K[X]= PIdlK[X]p"
    unfolding rupture_def FactRing_def by simp
  hence "𝟭K[X] PIdlK[X]p"
    using ideal.rcos_const_imp_mem[OF UP.cgenideal_ideal[OF assms(2)]] by auto
  then obtain q where "q  carrier (K[X])" and "𝟭K[X]= q K[X]p"
    using assms(2) unfolding cgenideal_def by auto
  hence "p  Units (K[X])"
    unfolding Units_def using assms(2) UP.m_comm by auto
  hence "degree p = 0"
    unfolding univ_poly_units[OF assms(1)] by auto
  with degree p > 0 show False
    by simp
qed

corollary (in ring) pirreducible_degree:
  assumes "subfield K R" "p  carrier (K[X])" "pirreducible K p"
  shows "degree p  1"
proof (rule ccontr)
  assume "¬ degree p  1" then have "length p  1"
    by simp
  moreover have "p  []" and "p  Units (K[X])"
    using assms(3) by (auto simp add: ring_irreducible_def irreducible_def univ_poly_zero)
  ultimately obtain k where k: "p = [ k ]"
    by (metis append_butlast_last_id butlast_take diff_is_0_eq le_refl self_append_conv2 take0 take_all)
  hence "k  K" and "k  𝟬"
    using assms(2) by (auto simp add: polynomial_def univ_poly_def)
  hence "p  Units (K[X])"
    using univ_poly_units[OF assms(1)] unfolding k by auto
  from p  Units (K[X]) and p  Units (K[X]) show False by simp
qed

corollary (in domain) univ_poly_not_field:
  assumes "subring K R" shows "¬ field (K[X])"
proof -
  have "X  carrier (K[X]) - { 𝟬(K[X])}" and "X  { [ k ] | k. k  K - { 𝟬 } }"
    using var_closed(1)[OF assms] unfolding univ_poly_zero var_def by auto 
  thus ?thesis
    using field.field_Units[of "K[X]"] univ_poly_units_incl[OF assms] by blast 
qed

lemma (in domain) rupture_is_field_iff_pirreducible:
  assumes "subfield K R" and "p  carrier (K[X])"
  shows "field (Rupt K p)  pirreducible K p"
proof
  assume "pirreducible K p" thus "field (Rupt K p)"
    using principal_domain.field_iff_prime[OF univ_poly_is_principal[OF assms(1)]] assms(2)
          pprime_iff_pirreducible[OF assms] pirreducibleE(1)[OF subfieldE(1)[OF assms(1)]]
    by (simp add: univ_poly_zero rupture_def)
next
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .

  assume field: "field (Rupt K p)"
  have "p  []"
  proof (rule ccontr)
    assume "¬ p  []" then have p: "p = []"
      by simp
    hence "Rupt K p  (K[X])"
      using UP.FactRing_zeroideal(1) UP.genideal_zero
            UP.cgenideal_eq_genideal[OF UP.zero_closed]
      by (simp add: rupture_def univ_poly_zero)
    then obtain h where h: "h  ring_iso (Rupt K p) (K[X])"
      unfolding is_ring_iso_def by blast
    moreover have "ring (Rupt K p)"
      using field by (simp add: cring_def domain_def field_def) 
    ultimately interpret R: ring_hom_ring "Rupt K p" "K[X]" h
      unfolding ring_hom_ring_def ring_hom_ring_axioms_def ring_iso_def
      using UP.ring_axioms by simp
    have "field (K[X])"
      using field.ring_iso_imp_img_field[OF field h] by simp
    thus False
      using univ_poly_not_field[OF subfieldE(1)[OF assms(1)]] by simp
  qed
  thus "pirreducible K p"
    using UP.field_iff_prime pprime_iff_pirreducible[OF assms] assms(2) field
    by (simp add: univ_poly_zero rupture_def)
qed

lemma (in domain) rupture_surj_hom:
  assumes "subring K R" and "p  carrier (K[X])"
  shows "(rupture_surj K p)  ring_hom (K[X]) (Rupt K p)"
    and "ring_hom_ring (K[X]) (Rupt K p) (rupture_surj K p)"
proof -
  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF assms(1)] .
  interpret I: ideal "PIdlK[X]p" "K[X]"
    using UP.cgenideal_ideal[OF assms(2)] .
  show "(rupture_surj K p)  ring_hom (K[X]) (Rupt K p)"
   and "ring_hom_ring (K[X]) (Rupt K p) (rupture_surj K p)"
    using ring_hom_ring.intro[OF UP.ring_axioms I.quotient_is_ring] I.rcos_ring_hom
    unfolding symmetric[OF ring_hom_ring_axioms_def] rupture_def by auto
qed

corollary (in domain) rupture_surj_norm_is_hom:
  assumes "subring K R" and "p  carrier (K[X])"
  shows "((rupture_surj K p)  poly_of_const)  ring_hom (R  carrier := K ) (Rupt K p)"
  using ring_hom_trans[OF canonical_embedding_is_hom[OF assms(1)] rupture_surj_hom(1)[OF assms]] .

lemma (in domain) norm_map_in_poly_ring_carrier:
  assumes "p  carrier (poly_ring R)" and "a. a  carrier R  f a  carrier (poly_ring R)"
  shows "ring.normalize (poly_ring R) (map f p)  carrier (poly_ring (poly_ring R))"
proof -
  have "set p  carrier R"
    using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  hence "set (map f p)  carrier (poly_ring R)"
    using assms(2) by auto
  thus ?thesis
    using ring.normalize_gives_polynomial[OF univ_poly_is_ring[OF carrier_is_subring]]
    unfolding univ_poly_carrier by simp
qed

lemma (in domain) map_in_poly_ring_carrier:
  assumes "p  carrier (poly_ring R)" and "a. a  carrier R  f a  carrier (poly_ring R)"
    and "a. a  𝟬  f a  []"
  shows "map f p  carrier (poly_ring (poly_ring R))"
proof -
  interpret UP: ring "poly_ring R"
    using univ_poly_is_ring[OF carrier_is_subring] .
  have "lead_coeff p  𝟬" if "p  []"
    using that assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  hence "ring.normalize (poly_ring R) (map f p) = map f p"
    by (cases p) (simp_all add: assms(3) univ_poly_zero)
  thus ?thesis
    using norm_map_in_poly_ring_carrier[of p f] assms(1-2) by simp
qed

lemma (in domain) map_norm_in_poly_ring_carrier:
  assumes "subring K R" and "p  carrier (K[X])"
  shows "map poly_of_const p  carrier (poly_ring (K[X]))"
  using domain.map_in_poly_ring_carrier[OF subring_is_domain[OF assms(1)]]
proof -
  have "a. a  K  poly_of_const a  carrier (K[X])"
   and "a. a  𝟬  poly_of_const a  []"
    using ring_hom_memE(1)[OF canonical_embedding_is_hom[OF assms(1)]]
    by (auto simp: poly_of_const_def)
  thus ?thesis
    using domain.map_in_poly_ring_carrier[OF subring_is_domain[OF assms(1)]] assms(2)
    unfolding univ_poly_consistent[OF assms(1)] by simp
qed

lemma (in domain) polynomial_rupture:
  assumes "subring K R" and "p  carrier (K[X])"
  shows "(ring.eval (Rupt K p)) (map ((rupture_surj K p)  poly_of_const) p) (rupture_surj K p X) = 𝟬Rupt K p⇙"
proof -
  let ?surj = "rupture_surj K p"

  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF assms(1)] .
  interpret Hom: ring_hom_ring "K[X]" "Rupt K p" ?surj
    using rupture_surj_hom(2)[OF assms] .

  have "(Hom.S.eval) (map (?surj  poly_of_const) p) (?surj X) = ?surj ((UP.eval) (map poly_of_const p) X)"
    using Hom.eval_hom[OF UP.carrier_is_subring var_closed(1)[OF assms(1)]
          map_norm_in_poly_ring_carrier[OF assms]] by simp
  also have " ... = ?surj p"
    unfolding sym[OF eval_rewrite[OF assms]] ..
  also have " ... = 𝟬Rupt K p⇙"
    using UP.a_rcos_zero[OF UP.cgenideal_ideal[OF assms(2)] UP.cgenideal_self[OF assms(2)]]
    unfolding rupture_def FactRing_def by simp
  finally show ?thesis .
qed


subsection ‹Division›

definition (in ring) long_divides :: "'a list  'a list  ('a list × 'a list)  bool"
  where "long_divides p q t 
           ― ‹i›   (t  carrier (poly_ring R) × carrier (poly_ring R)) 
           ― ‹ii›  (p = (q poly_ring R(fst t)) poly_ring R(snd t)) 
           ― ‹iii› (snd t = []  degree (snd t) < degree q)"

definition (in ring) long_division :: "'a list  'a list  ('a list × 'a list)"
  where "long_division p q = (THE t. long_divides p q t)"

definition (in ring) pdiv :: "'a list  'a list  'a list" (infixl pdiv 65)
  where "p pdiv q = (if q = [] then [] else fst (long_division p q))"

definition (in ring) pmod :: "'a list  'a list  'a list" (infixl pmod 65)
  where "p pmod q = (if q = [] then p else snd (long_division p q))"


lemma (in ring) long_dividesI:
  assumes "b  carrier (poly_ring R)" and "r  carrier (poly_ring R)"
      and "p = (q poly_ring Rb) poly_ring Rr" and "r = []  degree r < degree q"
    shows "long_divides p q (b, r)"
  using assms unfolding long_divides_def by auto 

lemma (in domain) exists_long_division:
  assumes "subfield K R" and "p  carrier (K[X])" and "q  carrier (K[X])" "q  []"
  obtains b r where "b  carrier (K[X])" and "r  carrier (K[X])" and "long_divides p q (b, r)"
  using subfield_long_division_theorem_shell[OF assms(1-3)] assms(4)
        carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)]]
  unfolding long_divides_def univ_poly_zero univ_poly_add univ_poly_mult by auto

lemma (in domain) exists_unique_long_division:
  assumes "subfield K R" and "p  carrier (K[X])" and "q  carrier (K[X])" "q  []"
  shows "∃!t. long_divides p q t"
proof -
  let ?padd   = "λa b. a poly_ring Rb"
  let ?pmult  = "λa b. a poly_ring Rb"
  let ?pminus = "λa b. a poly_ring Rb"

  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  obtain b r where ldiv: "long_divides p q (b, r)"
    using exists_long_division[OF assms] by metis

  moreover have "(b, r) = (b', r')" if "long_divides p q (b', r')" for b' r'
  proof -
    have q: "q  carrier (poly_ring R)" "q  []"
      using assms(3-4) carrier_polynomial[OF subfieldE(1)[OF assms(1)]]
      unfolding univ_poly_carrier by auto 
    hence in_carrier: "q  carrier (poly_ring R)"
      "b   carrier (poly_ring R)" "r   carrier (poly_ring R)"
      "b'  carrier (poly_ring R)" "r'  carrier (poly_ring R)" 
      using assms(3) that ldiv unfolding long_divides_def by auto
    have "?pminus (?padd (?pmult q b) r) r' = ?pminus (?padd (?pmult q b') r') r'"
      using ldiv and that unfolding long_divides_def by auto
    hence eq: "?padd (?pmult q (?pminus b b')) (?pminus r r') = 𝟬poly_ring R⇙"
      using in_carrier by algebra
    have "b = b'"
    proof (rule ccontr)
      assume "b  b'"
      hence pminus: "?pminus b b'  𝟬poly_ring R⇙" "?pminus b b'  carrier (poly_ring R)"
        using in_carrier(2,4) by (metis UP.add.inv_closed UP.l_neg UP.minus_eq UP.minus_unique, algebra)
      hence degree_ge: "degree (?pmult q (?pminus b b'))  degree q"
        using poly_mult_degree_eq[OF carrier_is_subring, of q "?pminus b b'"] q
        unfolding univ_poly_zero univ_poly_carrier univ_poly_mult by simp

      have "?pminus b b' = 𝟬poly_ring R⇙" if "?pminus r r' = 𝟬poly_ring R⇙"
        using eq pminus(2) q UP.integral univ_poly_zero unfolding that by auto 
      hence "?pminus r r'  []"
        using pminus(1) unfolding univ_poly_zero by blast
      moreover have "?pminus r r' = []" if "r = []" and "r' = []"
        using univ_poly_a_inv_def'[OF carrier_is_subring UP.zero_closed] that
        unfolding a_minus_def univ_poly_add univ_poly_zero by auto
      ultimately have "r  []  r'  []"
        by blast
      hence "max (degree r) (degree r') < degree q"
        using ldiv and that unfolding long_divides_def by auto
      moreover have "degree (?pminus r r')  max (degree r) (degree r')"
        using poly_add_degree[of r "map (a_inv R) r'"]
        unfolding a_minus_def univ_poly_add univ_poly_a_inv_def'[OF carrier_is_subring in_carrier(5)]
        by auto
      ultimately have degree_lt: "degree (?pminus r r') < degree q"
        by linarith
      have is_poly: "polynomial (carrier R) (?pmult q (?pminus b b'))" "polynomial (carrier R) (?pminus r r')"
        using in_carrier pminus(2) unfolding univ_poly_carrier by algebra+
      
      have "degree (?padd (?pmult q (?pminus b b')) (?pminus r r')) = degree (?pmult q (?pminus b b'))"
        using poly_add_degree_eq[OF carrier_is_subring is_poly] degree_ge degree_lt
        unfolding univ_poly_carrier sym[OF univ_poly_add[of R "carrier R"]] max_def by simp
      hence "degree (?padd (?pmult q (?pminus b b')) (?pminus r r')) > 0"
        using degree_ge degree_lt by simp
      moreover have "degree (?padd (?pmult q (?pminus b b')) (?pminus r r')) = 0"
        using eq unfolding univ_poly_zero by simp
      ultimately show False by simp
    qed
    hence "?pminus r r' = 𝟬poly_ring R⇙"
      using in_carrier eq by algebra
    hence "r = r'"
      using in_carrier by (metis UP.add.inv_closed UP.add.right_cancel UP.minus_eq UP.r_neg)
    with b = b' show ?thesis
      by simp
  qed

  ultimately show ?thesis
    by auto
qed

lemma (in domain) long_divisionE:
  assumes "subfield K R" and "p  carrier (K[X])" and "q  carrier (K[X])" "q  []"
  shows "long_divides p q (p pdiv q, p pmod q)"
  using theI'[OF exists_unique_long_division[OF assms]] assms(4)
  unfolding pmod_def pdiv_def long_division_def by auto

lemma (in domain) long_divisionI:
  assumes "subfield K R" and "p  carrier (K[X])" and "q  carrier (K[X])" "q  []"
  shows "long_divides p q (b, r)  (b, r) = (p pdiv q, p pmod q)"
  using exists_unique_long_division[OF assms] long_divisionE[OF assms] by metis

lemma (in domain) long_division_closed:
  assumes "subfield K R" and "p  carrier (K[X])" "q  carrier (K[X])"
  shows "p pdiv q  carrier (K[X])" and "p pmod q  carrier (K[X])"
proof -
  have "p pdiv q  carrier (K[X])  p pmod q  carrier (K[X])"
    using assms univ_poly_zero_closed[of R] long_divisionI[of K] exists_long_division[OF assms]
    by (cases "q = []") (simp add: pdiv_def pmod_def, metis Pair_inject)+
  thus "p pdiv q  carrier (K[X])" and "p pmod q  carrier (K[X])"
    by auto
qed

lemma (in domain) pdiv_pmod:
  assumes "subfield K R" and "p  carrier (K[X])" "q  carrier (K[X])"
  shows "p = (q K[X](p pdiv q)) K[X](p pmod q)"
proof (cases)
  interpret UP: ring "K[X]"
    using univ_poly_is_ring[OF subfieldE(1)[OF assms(1)]] .
  assume "q = []" thus ?thesis
    using assms(2) unfolding pdiv_def pmod_def sym[OF univ_poly_zero[of R K]] by simp
next
  assume "q  []" thus ?thesis
    using long_divisionE[OF assms] unfolding long_divides_def univ_poly_mult univ_poly_add by simp
qed

lemma (in domain) pmod_degree:
  assumes "subfield K R" and "p  carrier (K[X])" and "q  carrier (K[X])" "q  []"
  shows "p pmod q = []  degree (p pmod q) < degree q"
  using long_divisionE[OF assms] unfolding long_divides_def by auto

lemma (in domain) pmod_const:
  assumes "subfield K R" and "p  carrier (K[X])" "q  carrier (K[X])" and "degree q > degree p" 
  shows "p pdiv q = []" and "p pmod q = p"
proof -
  have "p pdiv q = []  p pmod q = p"
  proof (cases)
    interpret UP: ring "K[X]"
      using univ_poly_is_ring[OF subfieldE(1)[OF assms(1)]] .

    assume "q  []"
    have "p = (q K[X][]) K[X]p"
      using assms(2-3) unfolding sym[OF univ_poly_zero[of R K]] by simp
    moreover have "([], p)  carrier (poly_ring R) × carrier (poly_ring R)"
      using carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)] assms(2)] by auto
    ultimately have "long_divides p q ([], p)"
      using assms(4) unfolding long_divides_def univ_poly_mult univ_poly_add by auto
    with q  [] show ?thesis
      using long_divisionI[OF assms(1-3)] by auto
  qed (simp add: pmod_def pdiv_def)
  thus "p pdiv q = []" and "p pmod q = p"
    by auto
qed

lemma (in domain) long_division_zero:
  assumes "subfield K R" and "q  carrier (K[X])" shows "[] pdiv q = []" and "[] pmod q = []"
proof -
  interpret UP: ring "poly_ring R"
    using univ_poly_is_ring[OF carrier_is_subring] .

  have "[] pdiv q = []  [] pmod q = []"
  proof (cases)
    assume "q  []"
    have "q  carrier (poly_ring R)"
      using carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)] assms(2)] .
    hence "long_divides [] q ([], [])"
      unfolding long_divides_def sym[OF univ_poly_zero[of R "carrier R"]] by auto
    with q  [] show ?thesis
      using long_divisionI[OF assms(1) univ_poly_zero_closed assms(2)] by simp
  qed (simp add: pmod_def pdiv_def)
  thus "[] pdiv q = []" and "[] pmod q = []"
    by auto
qed

lemma (in domain) long_division_a_inv:
  assumes "subfield K R" and "p  carrier (K[X])" "q  carrier (K[X])"
  shows "((K[X]p) pdiv q) = K[X](p pdiv q)" (is "?pdiv")
    and "((K[X]p) pmod q) = K[X](p pmod q)" (is "?pmod")
proof -
  interpret UP: ring "K[X]"
    using univ_poly_is_ring[OF subfieldE(1)[OF assms(1)]] .

  have "?pdiv  ?pmod"
  proof (cases)
    assume "q = []" thus ?thesis
      unfolding pmod_def pdiv_def sym[OF univ_poly_zero[of R K]] by simp
  next
    assume not_nil: "q  []"
    have "K[X]p = K[X]((q K[X](p pdiv q)) K[X](p pmod q))"
      using pdiv_pmod[OF assms] by simp
    hence "K[X]p = (q K[X](K[X](p pdiv q))) K[X](K[X](p pmod q))"
      using assms(2-3) long_division_closed[OF assms] by algebra
    moreover have "K[X](p pdiv q)  carrier (K[X])" "K[X](p pmod q)  carrier (K[X])"
      using long_division_closed[OF assms] by algebra+
    hence "(K[X](p pdiv q), K[X](p pmod q))  carrier (poly_ring R) × carrier (poly_ring R)"
      using carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)]] by auto
    moreover have "K[X](p pmod q) = []  degree (K[X](p pmod q)) < degree q"
      using univ_poly_a_inv_length[OF subfieldE(1)[OF assms(1)]
            long_division_closed(2)[OF assms]] pmod_degree[OF assms not_nil]
      by auto
    ultimately have "long_divides (K[X]p) q (K[X](p pdiv q), K[X](p pmod q))"
      unfolding long_divides_def univ_poly_mult univ_poly_add by simp
    thus ?thesis
      using long_divisionI[OF assms(1) UP.a_inv_closed[OF assms(2)] assms(3) not_nil] by simp
  qed
  thus ?pdiv and ?pmod
    by auto
qed

lemma (in domain) long_division_add:
  assumes "subfield K R" and "a  carrier (K[X])" "b  carrier (K[X])" "q  carrier (K[X])"
  shows "(a K[X]b) pdiv q = (a pdiv q) K[X](b pdiv q)" (is "?pdiv")
    and "(a K[X]b) pmod q = (a pmod q) K[X](b pmod q)" (is "?pmod")
proof -
  let ?pdiv_add = "(a pdiv q) K[X](b pdiv q)"
  let ?pmod_add = "(a pmod q) K[X](b pmod q)"

  interpret UP: ring "K[X]"
    using univ_poly_is_ring[OF subfieldE(1)[OF assms(1)]] .

  have "?pdiv  ?pmod"
  proof (cases)
    assume "q = []" thus ?thesis
      using assms(2-3) unfolding pmod_def pdiv_def sym[OF univ_poly_zero[of R K]] by simp
  next
    note in_carrier = long_division_closed[OF assms(1,2,4)]
                      long_division_closed[OF assms(1,3,4)]

    assume "q  []"
    have "a K[X]b = ((q K[X](a pdiv q)) K[X](a pmod q)) K[X]((q K[X](b pdiv q)) K[X](b pmod q))"
      using assms(2-3)[THEN pdiv_pmod[OF assms(1) _ assms(4)]] by simp
    hence "a K[X]b = (q K[X]?pdiv_add) K[X]?pmod_add"
      using assms(4) in_carrier by algebra
    moreover have "(?pdiv_add, ?pmod_add)  carrier (poly_ring R) × carrier (poly_ring R)"
      using in_carrier carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)]] by auto
    moreover have "?pmod_add = []  degree ?pmod_add < degree q"
    proof (cases)
      assume "?pmod_add  []"
      hence "a pmod q  []  b pmod q  []"
        using in_carrier(2,4) unfolding sym[OF univ_poly_zero[of R K]] by auto
      moreover from q  []
      have "a pmod q = []  degree (a pmod q) < degree q" and "b pmod q = []  degree (b pmod q) < degree q"
        using assms(2-3)[THEN pmod_degree[OF assms(1) _ assms(4)]] by auto
      ultimately have "max (degree (a pmod q)) (degree (b pmod q)) < degree q"
        by auto
      thus ?thesis
        using poly_add_degree le_less_trans unfolding univ_poly_add by blast
    qed simp
    ultimately have "long_divides (a K[X]b) q (?pdiv_add, ?pmod_add)"
      unfolding long_divides_def univ_poly_mult univ_poly_add by simp
    with q  [] show ?thesis
      using long_divisionI[OF assms(1) UP.a_closed[OF assms(2-3)] assms(4)] by simp
  qed
  thus ?pdiv and ?pmod
    by auto
qed

lemma (in domain) long_division_add_iff:
  assumes "subfield K R"
    and "a  carrier (K[X])" "b  carrier (K[X])" "c  carrier (K[X])" "q  carrier (K[X])"
  shows "a pmod q = b pmod q  (a K[X]c) pmod q = (b K[X]c) pmod q"
proof -
  interpret UP: ring "K[X]"
    using univ_poly_is_ring[OF subfieldE(1)[OF assms(1)]] .
  show ?thesis
    using assms(2-4)[THEN long_division_closed(2)[OF assms(1) _ assms(5)]]
    unfolding assms(2-3)[THEN long_division_add(2)[OF assms(1) _ assms(4-5)]] by auto
qed

lemma (in domain) pdivides_iff:
  assumes "subfield K R" and "polynomial K p" "polynomial K q"
  shows "p pdivides q  p dividesK[X]q"
proof
  show "p dividesK [X]q  p pdivides q"
    using carrier_polynomial[OF subfieldE(1)[OF assms(1)]]
    unfolding pdivides_def factor_def univ_poly_mult univ_poly_carrier by auto
next
  interpret UP: ring "poly_ring R"
    using univ_poly_is_ring[OF carrier_is_subring] .
  
  have in_carrier: "p  carrier (poly_ring R)" "q  carrier (poly_ring R)"
    using carrier_polynomial[OF subfieldE(1)[OF assms(1)]] assms
    unfolding univ_poly_carrier by auto

  assume "p pdivides q"
  then obtain b where "b  carrier (poly_ring R)" and "q = p poly_ring Rb"
      unfolding pdivides_def factor_def by blast
  show "p dividesK[X]q"
  proof (cases)
    assume "p = []"
    with b  carrier (poly_ring R) and q = p poly_ring Rb have "q = []"
      unfolding univ_poly_mult sym[OF univ_poly_carrier]
      using poly_mult_zero(1)[OF polynomial_incl] by simp
    with p = [] show ?thesis
      using poly_mult_zero(2)[of "[]"]
      unfolding factor_def univ_poly_mult by auto 
  next
    interpret UP: ring "poly_ring R"
      using univ_poly_is_ring[OF carrier_is_subring] .

    assume "p  []"
    from p pdivides q obtain b where "b  carrier (poly_ring R)" and "q = p poly_ring Rb"
      unfolding pdivides_def factor_def by blast
    moreover have "p  carrier (poly_ring R)" and "q  carrier (poly_ring R)"
      using assms carrier_polynomial[OF subfieldE(1)[OF assms(1)]] unfolding univ_poly_carrier by auto
    ultimately have "q = (p poly_ring Rb) poly_ring R𝟬poly_ring R⇙"
      by algebra
    with b  carrier (poly_ring R) have "long_divides q p (b, [])"
      unfolding long_divides_def univ_poly_zero by auto
    with p  [] have "b  carrier (K[X])"
      using long_divisionI[of K q p b] long_division_closed[of K q p] assms
      unfolding univ_poly_carrier by auto
    with q = p poly_ring Rb show ?thesis
      unfolding factor_def univ_poly_mult by blast
  qed
qed

lemma (in domain) pdivides_iff_shell:
  assumes "subfield K R" and "p  carrier (K[X])" "q  carrier (K[X])"
  shows "p pdivides q  p dividesK[X]q"
  using pdivides_iff assms by (simp add: univ_poly_carrier)

lemma (in domain) pmod_zero_iff_pdivides:
  assumes "subfield K R" and "p  carrier (K[X])" "q  carrier (K[X])"
  shows "p pmod q = []  q pdivides p"
proof -
  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF subfieldE(1)[OF assms(1)]] .

  show ?thesis
  proof
    assume pmod: "p pmod q = []"
    have "p pdiv q  carrier (K[X])" and "p pmod q  carrier (K[X])"
      using long_division_closed[OF assms] by auto
    hence "p = q K[X](p pdiv q)"
      using pdiv_pmod[OF assms] assms(3) unfolding pmod sym[OF univ_poly_zero[of R K]] by algebra
    with p pdiv q  carrier (K[X]) show "q pdivides p"
      unfolding pdivides_iff_shell[OF assms(1,3,2)] factor_def by blast
  next
    assume "q pdivides p" show "p pmod q = []"
    proof (cases)
      assume "q = []" with q pdivides p show ?thesis
        using zero_pdivides unfolding pmod_def by simp
    next
      assume "q  []"
      from q pdivides p obtain r where "r  carrier (K[X])" and "p = q K[X]r"
        unfolding pdivides_iff_shell[OF assms(1,3,2)] factor_def by blast
      hence "p = (q K[X]r) K[X][]"
        using assms(2) unfolding sym[OF univ_poly_zero[of R K]] by simp
      moreover from r  carrier (K[X]) have "r  carrier (poly_ring R)"
        using carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)]] by auto
      ultimately have "long_divides p q (r, [])"
        unfolding long_divides_def univ_poly_mult univ_poly_add by auto
      with q  [] show ?thesis
        using long_divisionI[OF assms] by simp
    qed
  qed
qed

lemma (in domain) same_pmod_iff_pdivides:
  assumes "subfield K R" and "a  carrier (K[X])" "b  carrier (K[X])" "q  carrier (K[X])"
  shows "a pmod q = b pmod q  q pdivides (a K[X]b)"
proof -
  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF subfieldE(1)[OF assms(1)]] .

  have "a pmod q = b pmod q  (a K[X](K[X]b)) pmod q = (b K[X](K[X]b)) pmod q"
    using long_division_add_iff[OF assms(1-3) UP.a_inv_closed[OF assms(3)] assms(4)] .
  also have " ...  (a K[X]b) pmod q = 𝟬K[X]pmod q"
    using assms(2-3) by algebra
  also have " ...  q pdivides (a K[X]b)"
    using pmod_zero_iff_pdivides[OF assms(1) UP.minus_closed[OF assms(2-3)] assms(4)]
    unfolding univ_poly_zero long_division_zero(2)[OF assms(1,4)] .
  finally show ?thesis .
qed

lemma (in domain) pdivides_imp_degree_le:
  assumes "subring K R" and "p  carrier (K[X])" "q  carrier (K[X])" "q  []"
  shows "p pdivides q  degree p  degree q"
proof -
  assume "p pdivides q"
  then obtain r where r: "polynomial (carrier R) r" "q = poly_mult p r"
    unfolding pdivides_def factor_def univ_poly_mult univ_poly_carrier by blast
  moreover have p: "polynomial (carrier R) p"
    using assms(2) carrier_polynomial[OF assms(1)] unfolding univ_poly_carrier by auto
  moreover have "p  []" and "r  []"
    using poly_mult_zero(2)[OF polynomial_incl[OF p]] r(2) assms(4) by auto 
  ultimately show "degree p  degree q"
    using poly_mult_degree_eq[OF carrier_is_subring, of p r] by auto
qed

lemma (in domain) pprimeE:
  assumes "subfield K R" "p  carrier (K[X])" "pprime K p"
  shows "p  []" "p  Units (K[X])"
    and "q r.  q  carrier (K[X]); r  carrier (K[X]) 
                 p pdivides (q K[X]r)  p pdivides q  p pdivides r"
  using assms(2-3) poly_mult_closed[OF subfieldE(1)[OF assms(1)]] pdivides_iff[OF assms(1)]
  unfolding ring_prime_def prime_def 
  by (auto simp add: univ_poly_mult univ_poly_carrier univ_poly_zero)

lemma (in domain) pprimeI:
  assumes "subfield K R" "p  carrier (K[X])" "p  []" "p  Units (K[X])"
    and "q r.  q  carrier (K[X]); r  carrier (K[X]) 
                 p pdivides (q K[X]r)  p pdivides q  p pdivides r"
  shows "pprime K p"
  using assms(2-5) poly_mult_closed[OF subfieldE(1)[OF assms(1)]] pdivides_iff[OF assms(1)]
  unfolding ring_prime_def prime_def
  by (auto simp add: univ_poly_mult univ_poly_carrier univ_poly_zero)

lemma (in domain) associated_polynomials_iff:
  assumes "subfield K R" and "p  carrier (K[X])" "q  carrier (K[X])"
  shows "p K[X]q  (k  K - { 𝟬 }. p = [ k ] K[X]q)"
  using domain.ring_associated_iff[OF univ_poly_is_domain[OF subfieldE(1)[OF assms(1)]] assms(2-3)]
  unfolding univ_poly_units[OF assms(1)] by auto

corollary (in domain) associated_polynomials_imp_same_length: (* stronger than "imp_same_degree" *)
  assumes "subring K R" and "p  carrier (K[X])" and "q  carrier (K[X])"
  shows "p K[X]q  length p = length q"
proof -
  have aux_lemma: "length p  length q"
    if p: "p  carrier (K[X])" and q: "q  carrier (K[X])" and "p K[X]q" for p q
  proof (cases "q = []")
    case True with p K[X]q have "p = []"
      unfolding associated_def True factor_def univ_poly_def by auto
    thus ?thesis
      using True by simp
  next
    case False
    from p K[X]q have "p dividesK [X]q"
      unfolding associated_def by simp
    hence "p dividespoly_ring Rq"
      using carrier_polynomial[OF assms(1)]
      unfolding factor_def univ_poly_carrier univ_poly_mult by auto
    with q  [] have "degree p  degree q"
      using pdivides_imp_degree_le[OF assms(1) p q] unfolding pdivides_def by simp
    with q  [] show ?thesis
      by (cases "p = []", auto simp add: Suc_leI le_diff_iff)
  qed

  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF assms(1)] .

  assume "p K[X]q" thus ?thesis
    using aux_lemma[OF assms(2-3)] aux_lemma[OF assms(3,2) UP.associated_sym] by simp
qed

lemma (in ring) divides_pirreducible_condition:
  assumes "pirreducible K q" and "p  carrier (K[X])"
  shows "p dividesK[X]q  p  Units (K[X])  p K[X]q"
  using divides_irreducible_condition[of "K[X]" q p] assms
  unfolding ring_irreducible_def by auto

subsection ‹Polynomial Power›

lemma (in domain) polynomial_pow_not_zero:
  assumes "p  carrier (poly_ring R)" and "p  []"
  shows "p [^]poly_ring R(n::nat)  []"
proof -
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  from assms UP.integral show ?thesis
    unfolding sym[OF univ_poly_zero[of R "carrier R"]]
    by (induction n, auto)
qed

lemma (in domain) subring_polynomial_pow_not_zero:
  assumes "subring K R" and "p  carrier (K[X])" and "p  []"
  shows "p [^]K[X](n::nat)  []"
  using domain.polynomial_pow_not_zero[OF subring_is_domain, of K p n] assms
  unfolding univ_poly_consistent[OF assms(1)] by simp

lemma (in domain) polynomial_pow_degree:
  assumes "p  carrier (poly_ring R)"
  shows "degree (p [^]poly_ring Rn) = n * degree p"
proof -
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  show ?thesis
  proof (induction n)
    case 0 thus ?case
      using UP.nat_pow_0 unfolding univ_poly_one by auto
  next
    let ?ppow = "λn. p [^]poly_ring Rn"
    case (Suc n) thus ?case
    proof (cases "p = []")
      case True thus ?thesis
        using univ_poly_zero[of R "carrier R"] UP.r_null assms by auto
    next
      case False
      hence "?ppow n  carrier (poly_ring R)" and "?ppow n  []" and "p  []"
        using polynomial_pow_not_zero[of p n] assms by (auto simp add: univ_poly_one)
      thus ?thesis
        using poly_mult_degree_eq[OF carrier_is_subring, of "?ppow n" p] Suc assms
        unfolding univ_poly_carrier univ_poly_zero
        by (auto simp add: add.commute univ_poly_mult)
    qed
  qed
qed

lemma (in domain) subring_polynomial_pow_degree:
  assumes "subring K R" and "p  carrier (K[X])"
  shows "degree (p [^]K[X]n) = n * degree p"
  using domain.polynomial_pow_degree[OF subring_is_domain, of K p n] assms
  unfolding univ_poly_consistent[OF assms(1)] by simp

lemma (in domain) polynomial_pow_division:
  assumes "p  carrier (poly_ring R)" and "(n::nat)  m"
  shows "(p [^]poly_ring Rn) pdivides (p [^]poly_ring Rm)"
proof -
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  let ?ppow = "λn. p [^]poly_ring Rn"

  have "?ppow n poly_ring R?ppow k = ?ppow (n + k)" for k
    using assms(1) by (simp add: UP.nat_pow_mult)
  thus ?thesis
    using dividesI[of "?ppow (m - n)" "poly_ring R" "?ppow m" "?ppow n"] assms
    unfolding pdivides_def by auto
qed

lemma (in domain) subring_polynomial_pow_division:
  assumes "subring K R" and "p  carrier (K[X])" and "(n::nat)  m"
  shows "(p [^]K[X]n) dividesK[X](p [^]K[X]m)"
  using domain.polynomial_pow_division[OF subring_is_domain, of K p n m] assms
  unfolding univ_poly_consistent[OF assms(1)] pdivides_def by simp

lemma (in domain) pirreducible_pow_pdivides_iff:
  assumes "subfield K R" "p  carrier (K[X])" "q  carrier (K[X])" "r  carrier (K[X])"
    and "pirreducible K p" and "¬ (p pdivides q)"
  shows "(p [^]K[X](n :: nat)) pdivides (q K[X]r)  (p [^]K[X]n) pdivides r"
proof -
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .
  show ?thesis
  proof (cases "r = []")
    case True with q  carrier (K[X]) have "q K[X]r = []" and "r = []"
      unfolding  sym[OF univ_poly_zero[of R K]] by auto
    thus ?thesis
      using pdivides_zero[OF subfieldE(1),of K] assms by auto
  next
    case False then have not_zero: "p  []" "q  []" "r  []" "q K[X]r  []"
      using subfieldE(1) pdivides_zero[OF _ assms(2)] assms(1-2,5-6) pirreducibleE(1)
            UP.integral_iff[OF assms(3-4)] univ_poly_zero[of R K] by auto
    from p  []
    have ppow: "p [^]K[X](n :: nat)  []" "p [^]K[X](n :: nat)  carrier (K[X])"
      using subring_polynomial_pow_not_zero[OF subfieldE(1)] assms(1-2) by auto
    have not_pdiv: "¬ (p dividesmult_of (K[X])q)"
      using assms(6) pdivides_iff_shell[OF assms(1-3)] unfolding pdivides_def by auto
    have prime: "prime (mult_of (K[X])) p"
      using assms(5) pprime_iff_pirreducible[OF assms(1-2)]
      unfolding sym[OF UP.prime_eq_prime_mult[OF assms(2)]] ring_prime_def by simp
    have "a pdivides b  a dividesmult_of (K[X])b"
      if "a  carrier (K[X])" "a  𝟬K[X]⇙" "b  carrier (K[X])" "b  𝟬K[X]⇙" for a b
      using that UP.divides_imp_divides_mult[of a b] divides_mult_imp_divides[of "K[X]" a b]
      unfolding pdivides_iff_shell[OF assms(1) that(1,3)] by blast
    thus ?thesis
      using UP.mult_of.prime_pow_divides_iff[OF _ _ _ prime not_pdiv, of r] ppow not_zero assms(2-4)
      unfolding nat_pow_mult_of carrier_mult_of mult_mult_of sym[OF univ_poly_zero[of R K]]
      by (metis DiffI UP.m_closed singletonD)
  qed
qed

lemma (in domain) subring_degree_one_imp_pirreducible:
  assumes "subring K R" and "a  Units (R  carrier := K )" and "b  K"
  shows "pirreducible K [ a, b ]"
proof (rule pirreducibleI[OF assms(1)])
  have "a  K" and "a  𝟬"
    using assms(2) subringE(1)[OF assms(1)] unfolding Units_def by auto
  thus "[ a, b ]  carrier (K[X])" and "[ a, b ]  []" and "[ a, b ]  Units (K [X])"
    using univ_poly_units_incl[OF assms(1)] assms(2-3)
    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
next
  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF assms(1)] .

  have aux_lemma1: "degree q + degree r = 1" "q  []" "r  []"
    if q: "q  carrier (K[X])" and r: "r  carrier (K[X])" and "[ a, b ] = q K[X]r" for q r
  proof -
    from that have not_zero: "q  []" "r  []"
      by (metis UP.integral_iff list.distinct(1) univ_poly_zero)+
    have "degree (q K[X]r) = degree q + degree r"
      using not_zero poly_mult_degree_eq[OF assms(1)] q r
      by (simp add: univ_poly_carrier univ_poly_mult)
    with sym[OF [ a, b ] = q K[X]r] show "degree q + degree r = 1" and "q  []" "r  []"
      using not_zero by auto
  qed

  have aux_lemma2: "r  Units (K[X])"
    if q: "q  carrier (K[X])" "q  []" and r: "r  carrier (K[X])" "r  []"
    and "[ a, b ] = q K[X]r" and "degree q = 1" and "degree r = 0" for q r
  proof -
    from that have "length q = Suc (Suc 0)" and "length r = Suc 0"
      by (linarith, metis add.right_neutral add_eq_if length_0_conv)
    from length q = Suc (Suc 0) obtain c d where q_def: "q = [ c, d ]"
      by (metis length_0_conv length_Cons list.exhaust nat.inject)
    from length r = Suc 0 obtain e where r_def: "r = [ e ]"
      by (metis length_0_conv length_Suc_conv)
    from r = [ e ] and q = [ c, d ]
    have c: "c  K" "c  𝟬" and d: "d  K" and e: "e  K" "e  𝟬"
      using r q subringE(1)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto
    with sym[OF [ a, b ] = q K[X]r] have "a = c  e"
      using poly_mult_lead_coeff[OF assms(1), of q r]
      unfolding polynomial_def sym[OF univ_poly_mult[of R K]] r_def q_def by auto
    obtain inv_a where a: "a  K" and inv_a: "inv_a  K" "a  inv_a = 𝟭" "inv_a  a = 𝟭"
      using assms(2) unfolding Units_def by auto
    hence "a  𝟬" and "inv_a  𝟬"
      using subringE(1)[OF assms(1)] integral_iff by auto
    with c  K and c  𝟬 have in_carrier: "[ c  inv_a ]  carrier (K[X])"
      using subringE(1,6)[OF assms(1)] inv_a integral
      unfolding sym[OF univ_poly_carrier] polynomial_def
      by (auto, meson subsetD)
    moreover have "[ c  inv_a ] K[X]r = [ 𝟭 ]"
      using a = c  e a inv_a c e subsetD[OF subringE(1)[OF assms(1)]]
      unfolding r_def univ_poly_mult by (auto) (simp add: m_assoc m_lcomm integral_iff)+
    ultimately show ?thesis
      using r(1) UP.m_comm[OF in_carrier r(1)] unfolding sym[OF univ_poly_one[of R K]] Units_def by auto
  qed

  fix q r
  assume q: "q  carrier (K[X])" and r: "r  carrier (K[X])" and qr: "[ a, b ] = q K[X]r"
  thus "q  Units (K[X])  r  Units (K[X])"
    using aux_lemma1[OF q r qr] aux_lemma2[of q r] aux_lemma2[of r q] UP.m_comm add_is_1 by auto
qed

lemma (in domain) degree_one_imp_pirreducible:
  assumes "subfield K R" and "p  carrier (K[X])" and "degree p = 1"
  shows "pirreducible K p"
proof -
  from degree p = 1 have "length p = Suc (Suc 0)"
    by simp
  then obtain a b where p: "p = [ a, b ]"
    by (metis length_0_conv length_Cons nat.inject neq_Nil_conv)
  with p  carrier (K[X]) show ?thesis
    using subring_degree_one_imp_pirreducible[OF subfieldE(1)[OF assms(1)], of a b]
          subfield.subfield_Units[OF assms(1)]
    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
qed

lemma (in ring) degree_oneE[elim]:
  assumes "p  carrier (K[X])" and "degree p = 1"
    and "a b.  a  K; a  𝟬; b  K; p = [ a, b ]   P"
  shows P
proof -
  from degree p = 1 have "length p = Suc (Suc 0)"
    by simp
  then obtain a b where "p = [ a, b ]"
    by (metis length_0_conv length_Cons nat.inject neq_Nil_conv)
  with p  carrier (K[X]) have "a  K" and "a  𝟬" and "b  K"
    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  with p = [ a, b ] show ?thesis
    using assms(3) by simp
qed

lemma (in domain) subring_degree_one_associatedI:
  assumes "subring K R" and "a  K" "a'  K" and "b  K" and "a  a' = 𝟭"
  shows "[ a , b ] K[X][ 𝟭, a'  b ]"
proof -
  from a  a' = 𝟭 have not_zero: "a  𝟬" "a'  𝟬"
    using subringE(1)[OF assms(1)] assms(2-3) by auto
  hence "[ a, b ] = [ a ] K[X][ 𝟭, a'  b ]"
    using assms(2-4)[THEN subsetD[OF subringE(1)[OF assms(1)]]] assms(5) m_assoc
    unfolding univ_poly_mult by fastforce
  moreover have "[ a, b ]  carrier (K[X])" and "[ 𝟭, a'  b ]  carrier (K[X])"
    using subringE(1,3,6)[OF assms(1)] not_zero one_not_zero assms
    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  moreover have "[ a ]  Units (K[X])"
  proof -
    from a  𝟬 and a'  𝟬 have "[ a ]  carrier (K[X])" and "[ a' ]  carrier (K[X])"
      using assms(2-3) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
    moreover have "a'  a = 𝟭"
      using subsetD[OF subringE(1)[OF assms(1)]] assms m_comm by simp 
    hence "[ a ] K[X][ a' ] = [ 𝟭 ]" and "[ a' ] K[X][ a ] = [ 𝟭 ]"
      using assms unfolding univ_poly_mult by auto
    ultimately show ?thesis
      unfolding sym[OF univ_poly_one[of R K]] Units_def by blast
  qed
  ultimately show ?thesis
    using domain.ring_associated_iff[OF univ_poly_is_domain[OF assms(1)]] by blast
qed

lemma (in domain) degree_one_associatedI:
  assumes "subfield K R" and "p  carrier (K[X])" and "degree p = 1"
  shows "p K[X][ 𝟭, inv (lead_coeff p)  (const_term p) ]"
proof -
  from p  carrier (K[X]) and degree p = 1
  obtain a b where "p = [ a, b ]" and "a  K" "a  𝟬" and "b  K"
    by auto
  thus ?thesis
    using subring_degree_one_associatedI[OF subfieldE(1)[OF assms(1)]]
          subfield_m_inv[OF assms(1)] subsetD[OF subfieldE(3)[OF assms(1)]]
    unfolding const_term_def
    by auto
qed

subsection ‹Ideals›

lemma (in domain) exists_unique_gen:
  assumes "subfield K R" "ideal I (K[X])" "I  { [] }"
  shows "∃!p  carrier (K[X]). lead_coeff p = 𝟭  I = PIdlK[X]p"
    (is "∃!p. ?generator p")
proof -
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .
  obtain q where q: "q  carrier (K[X])" "I = PIdlK[X]q"
    using UP.exists_gen[OF assms(2)] by blast
  hence not_nil: "q  []"
    using UP.genideal_zero UP.cgenideal_eq_genideal[OF UP.zero_closed] assms(3)
    by (auto simp add: univ_poly_zero)
  hence "lead_coeff q  K - { 𝟬 }"
    using q(1) unfolding univ_poly_def polynomial_def by auto
  hence inv_lc_q: "inv (lead_coeff q)  K - { 𝟬 }" "inv (lead_coeff q)  lead_coeff q = 𝟭"
    using subfield_m_inv[OF assms(1)] by auto 

  define p where "p = [ inv (lead_coeff q) ] K[X]q"
  have is_poly: "polynomial K [ inv (lead_coeff q) ]" "polynomial K q"
    using inv_lc_q(1) q(1) unfolding univ_poly_def polynomial_def by auto
  hence in_carrier: "p  carrier (K[X])"
    using UP.m_closed unfolding univ_poly_carrier p_def by simp
  have lc_p: "lead_coeff p = 𝟭"
    using poly_mult_lead_coeff[OF subfieldE(1)[OF assms(1)] is_poly _ not_nil] inv_lc_q(2)
    unfolding p_def univ_poly_mult[of R K] by simp
  moreover have PIdl_p: "I = PIdlK[X]p"
    using UP.associated_iff_same_ideal[OF in_carrier q(1)] q(2) inv_lc_q(1) p_def
          associated_polynomials_iff[OF assms(1) in_carrier q(1)]
    by auto
  ultimately have "?generator p"
    using in_carrier by simp

  moreover
  have "r.  r  carrier (K[X]); lead_coeff r = 𝟭; I = PIdlK[X]r   r = p"
  proof -
    fix r assume r: "r  carrier (K[X])" "lead_coeff r = 𝟭" "I = PIdlK[X]r"
    have "subring K R"
      by (simp add: subfield K R subfieldE(1))
    obtain k where k: "k  K - { 𝟬 }" "r = [ k ] K[X]p"
      using UP.associated_iff_same_ideal[OF r(1) in_carrier] PIdl_p r(3)
            associated_polynomials_iff[OF assms(1) r(1) in_carrier]
      by auto
    hence "polynomial K [ k ]"
      unfolding polynomial_def by simp
    moreover have "p  []"
      using not_nil UP.associated_iff_same_ideal[OF in_carrier q(1)] q(2) PIdl_p
            associated_polynomials_imp_same_length[OF subring K R in_carrier q(1)] by auto
    ultimately have "lead_coeff r = k  (lead_coeff p)"
      using poly_mult_lead_coeff[OF subfieldE(1)[OF assms(1)]] in_carrier k(2)
      unfolding univ_poly_def by (auto simp del: poly_mult.simps)
    hence "k = 𝟭"
      using lc_p r(2) k(1) subfieldE(3)[OF assms(1)] by auto
    hence "r = map ((⊗) 𝟭) p"
      using poly_mult_const(1)[OF subfieldE(1)[OF assms(1)] _ k(1), of p] in_carrier
      unfolding k(2) univ_poly_carrier[of R K] univ_poly_mult[of R K] by auto
    moreover have "set p  carrier R"
      using polynomial_in_carrier[OF subfieldE(1)[OF assms(1)]]
            in_carrier univ_poly_carrier[of R K] by auto
    hence "map ((⊗) 𝟭) p = p"
      by (induct p) (auto)
    ultimately show "r = p" by simp
  qed

  ultimately show ?thesis by blast
qed

proposition (in domain) exists_unique_pirreducible_gen:
  assumes "subfield K R" "ring_hom_ring (K[X]) R h"
    and "a_kernel (K[X]) R h  { [] }" "a_kernel (K[X]) R h  carrier (K[X])"
  shows "∃!p  carrier (K[X]). pirreducible K p  lead_coeff p = 𝟭  a_kernel (K[X]) R h = PIdlK[X]p"
    (is "∃!p. ?generator p")
proof -
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .

  have "ideal (a_kernel (K[X]) R h) (K[X])"
    using ring_hom_ring.kernel_is_ideal[OF assms(2)] .
  then obtain p
    where p: "p  carrier (K[X])" "lead_coeff p = 𝟭" "a_kernel (K[X]) R h = PIdlK[X]p"
      and unique:
      "q.  q  carrier (K[X]); lead_coeff q = 𝟭; a_kernel (K[X]) R h = PIdlK[X]q   q = p"
    using exists_unique_gen[OF assms(1) _ assms(3)] by metis

  have "p  carrier (K[X]) - { [] }"
      using UP.genideal_zero UP.cgenideal_eq_genideal[OF UP.zero_closed] assms(3) p(1,3)
      by (auto simp add: univ_poly_zero)
  hence "pprime K p"
    using ring_hom_ring.primeideal_vimage[OF assms(2) UP.is_cring zeroprimeideal]
          UP.primeideal_iff_prime[of p]
    unfolding univ_poly_zero sym[OF p(3)] a_kernel_def' by simp
  hence "pirreducible K p"
    using pprime_iff_pirreducible[OF assms(1) p(1)] by simp
  thus ?thesis
    using p unique by metis 
qed

lemma (in domain) cgenideal_pirreducible:
  assumes "subfield K R" and "p  carrier (K[X])" "pirreducible K p" 
  shows " pirreducible K q; q  PIdlK[X]p   p K[X]q"
proof -
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .

  assume q: "pirreducible K q" "q  PIdlK[X]p"
  hence in_carrier: "q  carrier (K[X])"
    using additive_subgroup.a_subset[OF ideal.axioms(1)[OF UP.cgenideal_ideal[OF assms(2)]]] by auto
  hence "p dividesK[X]q"
    by (meson q assms(2) UP.cgenideal_ideal UP.cgenideal_minimal UP.to_contain_is_to_divide)
  then obtain r where r: "r  carrier (K[X])" "q = p K[X]r"
    by auto
  hence "r  Units (K[X])"
    using pirreducibleE(3)[OF _ in_carrier q(1) assms(2) r(1)] subfieldE(1)[OF assms(1)]
          pirreducibleE(2)[OF _ assms(2-3)] by auto
  thus "p K[X]q"
    using UP.ring_associated_iff[OF in_carrier assms(2)] r(2) UP.associated_sym
    unfolding UP.m_comm[OF assms(2) r(1)] by auto
qed


subsection ‹Roots and Multiplicity›

definition (in ring) is_root :: "'a list  'a  bool"
  where "is_root p x  (x  carrier R  eval p x = 𝟬  p  [])"

definition (in ring) alg_mult :: "'a list  'a  nat"
  where "alg_mult p x =
           (if p = [] then 0 else
             (if x  carrier R then Greatest (λ n. ([ 𝟭,  x ] [^]poly_ring Rn) pdivides p) else 0))"

definition (in ring) roots :: "'a list  'a multiset"
  where "roots p =