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 "pirreducible⇘R⇙ K p ≡ ring_irreducible⇘(univ_poly R K)⇙ p"

abbreviation pprime :: "_ ⇒ 'a set ⇒ 'a list ⇒ bool" ("pprimeı")
  where "pprime⇘R⇙ K p ≡ ring_prime⇘(univ_poly R K)⇙ p"

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

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

abbreviation (in ring) rupture_surj :: "'a set ⇒ 'a list ⇒ 'a list ⇒ ('a list) set"
  where "rupture_surj K p ≡ (λq. (PIdl⇘K[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 "PIdl⇘K[X]⇙ p +>⇘K[X]⇙ 𝟭⇘K[X]⇙ = PIdl⇘K[X]⇙ p"
    unfolding rupture_def FactRing_def by simp
  hence "𝟭⇘K[X]⇙ ∈ PIdl⇘K[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 "PIdl⇘K[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 R⇙ b) ⊕⇘poly_ring R⇙ r" 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 R⇙ b"
  let ?pmult  = "λa b. a ⊗⇘poly_ring R⇙ b"
  let ?pminus = "λa b. a ⊖⇘poly_ring R⇙ b"

  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 divides⇘K[X]⇙ q"
proof
  show "p divides⇘K [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 R⇙ b"
      unfolding pdivides_def factor_def by blast
  show "p divides⇘K[X]⇙ q"
  proof (cases)
    assume "p = []"
    with ‹b ∈ carrier (poly_ring R)› and ‹q = p ⊗⇘poly_ring R⇙ b› 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 R⇙ b"
      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 R⇙ b) ⊕⇘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 R⇙ b› 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 divides⇘K[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 -
  { fix p q
    assume p: "p ∈ carrier (K[X])" and q: "q ∈ carrier (K[X])" and "p ∼⇘K[X]⇙ q"
    have "length p ≤ length 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 divides⇘K [X]⇙ q"
        unfolding associated_def by simp
      hence "p divides⇘poly_ring R⇙ q"
        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
  } note aux_lemma = this

  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 divides⇘K[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 R⇙ n) = 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 R⇙ n"
    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 R⇙ n) pdivides (p [^]⇘poly_ring R⇙ m)"
proof -
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  let ?ppow = "λn. p [^]⇘poly_ring R⇙ n"

  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) divides⇘K[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 divides⇘mult_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 divides⇘mult_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)] .

  { fix q r
    assume q: "q ∈ carrier (K[X])" and r: "r ∈ carrier (K[X])" and "[ a, b ] = q ⊗⇘K[X]⇙ r"
    hence 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›] have "degree q + degree r = 1" and "q ≠ []" "r ≠ []"
      using not_zero by auto
  } note aux_lemma1 = this

  { fix q r
    assume 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"
    hence "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 have "r ∈ Units (K[X])"
      using r(1) UP.m_comm[OF in_carrier r(1)] unfolding sym[OF univ_poly_one[of R K]] Units_def by auto
  } note aux_lemma2 = this

  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 = PIdl⇘K[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 = PIdl⇘K[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 = PIdl⇘K[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 = PIdl⇘K[X]⇙ r ⟧ ⟹ r = p"
  proof -
    fix r assume r: "r ∈ carrier (K[X])" "lead_coeff r = 𝟭" "I = PIdl⇘K[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 = PIdl⇘K[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 = PIdl⇘K[X]⇙ p"
      and unique:
      "⋀q. ⟦ q ∈ carrier (K[X]); lead_coeff q = 𝟭; a_kernel (K[X]) R h = PIdl⇘K[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 ∈ PIdl⇘K[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 ∈ PIdl⇘K[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 divides⇘K[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 R⇙ n) pdivides p) else 0))"

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

definition (in ring) roots_on :: "'a set ⇒ 'a list ⇒ 'a multiset"
  where "roots_on K p = roots p ∩# mset_set K"

definition (in ring) splitted :: "'a list ⇒ bool"
  where "splitted p ⟷ size (roots p) = degree p"

definition (in ring) splitted_on :: "'a set ⇒ 'a list ⇒ bool"
  where "splitted_on K p ⟷ size (roots_on K p) = degree p"

lemma (in domain) pdivides_imp_root_sharing:
  assumes "p ∈ carrier (poly_ring R)" "p pdivides q" and "a ∈ carrier R"
  shows "eval p a = 𝟬 ⟹ eval q a = 𝟬"
proof - 
  from ‹p pdivides q› obtain r where r: "q = p ⊗⇘poly_ring R⇙ r" "r ∈ carrier (poly_ring R)"
    unfolding pdivides_def factor_def by auto
  hence "eval q a = (eval p a) ⊗ (eval r a)"
    using ring_hom_memE(2)[OF eval_is_hom[OF carrier_is_subring assms(3)] assms(1) r(2)] by simp
  thus "eval p a = 𝟬 ⟹ eval q a = 𝟬"
    using ring_hom_memE(1)[OF eval_is_hom[OF carrier_is_subring assms(3)] r(2)] by auto
qed

lemma (in domain) degree_one_root:
  assumes "subfield K R" and "p ∈ carrier (K[X])" and "degree p = 1"
  shows "eval p (⊖ (inv (lead_coeff p) ⊗ (const_term p))) = 𝟬"
    and "inv (lead_coeff p) ⊗ (const_term p) ∈ K" 
proof -
  from ‹degree p = 1› have "length p = Suc (Suc 0)"
    by simp
  then obtain a b where p: "p = [ a, b ]"
    by (metis (no_types, opaque_lifting) Suc_length_conv length_0_conv)
  hence "a ∈ K - { 𝟬 }" "b ∈ K"  and in_carrier: "a ∈ carrier R" "b ∈ carrier R"
    using assms(2) subfieldE(3)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  hence inv_a: "inv a ∈ carrier R" "a ⊗ inv a = 𝟭" and "inv a ∈ K"
    using subfield_m_inv(1-2)[OF assms(1), of a] subfieldE(3)[OF assms(1)] by auto 
  hence "eval p (⊖ (inv a ⊗ b)) = a ⊗ (⊖ (inv a ⊗ b)) ⊕ b"
    using in_carrier unfolding p by simp
  also have " ... = ⊖ (a ⊗ (inv a ⊗ b)) ⊕ b"
    using inv_a in_carrier by (simp add: r_minus)
  also have " ... = 𝟬"
    using in_carrier(2) unfolding sym[OF m_assoc[OF in_carrier(1) inv_a(1) in_carrier(2)]] inv_a(2) by algebra
  finally have "eval p (⊖ (inv a ⊗ b)) = 𝟬" .
  moreover have ct: "const_term p = b"
    using in_carrier unfolding p const_term_def by auto
  ultimately show "eval p (⊖ (inv (lead_coeff p) ⊗ (const_term p))) = 𝟬"
    unfolding p by simp
  from ‹inv a ∈ K› and ‹b ∈ K›
  show "inv (lead_coeff p) ⊗ (const_term p) ∈ K"
    using p subringE(6)[OF subfieldE(1)[OF assms(1)]] unfolding ct by auto
qed
lemma (in domain) is_root_imp_pdivides:
  assumes "p ∈ carrier (poly_ring R)"
  shows "is_root p x ⟹ [ 𝟭, ⊖ x ] pdivides p"
proof -
  let ?b = "[ 𝟭 , ⊖ x ]"

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

  assume "is_root p x" hence x: "x ∈ carrier R" and is_root: "eval p x = 𝟬"
    unfolding is_root_def by auto
  hence b: "?b ∈ carrier (poly_ring R)"
    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  then obtain q r where q: "q ∈ carrier (poly_ring R)" and r: "r ∈ carrier (poly_ring R)"
    and long_divides: "p = (?b ⊗⇘poly_ring R⇙ q) ⊕⇘poly_ring R⇙ r" "r = [] ∨ degree r < degree ?b"
    using long_division_theorem[OF carrier_is_subring, of p ?b] assms by (auto simp add: univ_poly_carrier)

  show ?thesis
  proof (cases "r = []")
    case True then have "r = 𝟬⇘poly_ring R⇙"
      unfolding univ_poly_zero[of R "carrier R"] .
    thus ?thesis
      using long_divides(1) q r b dividesI[OF q, of p ?b] by (simp add: pdivides_def)
  next
    case False then have "length r = Suc 0"
      using long_divides(2) le_SucE by fastforce
    then obtain a where "r = [ a ]" and a: "a ∈ carrier R" and "a ≠ 𝟬"
      using r unfolding sym[OF univ_poly_carrier] polynomial_def
      by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))

    have "eval p x = ((eval ?b x) ⊗ (eval q x)) ⊕ (eval r x)"
      using long_divides(1) ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] by (simp add: b q r)
    also have " ... = eval r x"
      using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] x b q r by (auto, algebra)
    finally have "a = 𝟬"
      using a unfolding ‹r = [ a ]› is_root by simp
    with ‹a ≠ 𝟬› have False .. thus ?thesis ..
  qed
qed

lemma (in domain) pdivides_imp_is_root:
  assumes "p ≠ []" and "x ∈ carrier R"
  shows "[ 𝟭, ⊖ x ] pdivides p ⟹ is_root p x"
proof -
  assume "[ 𝟭, ⊖ x ] pdivides p"
  then obtain q where q: "q ∈ carrier (poly_ring R)" and pdiv: "p = [ 𝟭, ⊖ x ] ⊗⇘poly_ring R⇙ q"
    unfolding pdivides_def by auto
  moreover have "[ 𝟭, ⊖ x ] ∈ carrier (poly_ring R)"
    using assms(2) unfolding sym[OF univ_poly_carrier] polynomial_def by simp
  ultimately have "eval p x = 𝟬"
    using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring, of x]] assms(2) by (auto, algebra)
  with ‹p ≠ []› and ‹x ∈ carrier R› show "is_root p x"
    unfolding is_root_def by simp 
qed

lemma (in domain) associated_polynomials_imp_same_is_root:
  assumes "p ∈ carrier (poly_ring R)" and "q ∈ carrier (poly_ring R)" and "p ∼⇘poly_ring R⇙ q"
  shows "is_root p x ⟷ is_root q x"
proof (cases "p = []")
  case True with ‹p ∼⇘poly_ring R⇙ q› have "q = []"
    unfolding associated_def True factor_def univ_poly_def by auto
  thus ?thesis
    using True unfolding is_root_def by simp 
next
  case False
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  { fix p q
    assume p: "p ∈ carrier (poly_ring R)" and q: "q ∈ carrier (poly_ring R)" and pq: "p ∼⇘poly_ring R⇙ q"
    have "is_root p x ⟹ is_root q x"
    proof -
      assume is_root: "is_root p x"
      then have "[ 𝟭, ⊖ x ] pdivides p" and "p ≠ []" and "x ∈ carrier R"
        using is_root_imp_pdivides[OF p] unfolding is_root_def by auto
      moreover have "[ 𝟭, ⊖ x ] ∈ carrier (poly_ring R)"
        using is_root unfolding is_root_def sym[OF univ_poly_carrier] polynomial_def by simp
      ultimately have "[ 𝟭, ⊖ x ] pdivides q"
        using UP.divides_cong_r[OF _ pq ] unfolding pdivides_def by simp
      with ‹p ≠ []› and ‹x ∈ carrier R› show ?thesis
        using associated_polynomials_imp_same_length[OF carrier_is_subring p q pq]
              pdivides_imp_is_root[of q x]
        by fastforce  
    qed
  }

  then show ?thesis
    using assms UP.associated_sym[OF assms(3)] by blast 
qed

lemma (in ring) monic_degree_one_root_condition:
  assumes "a ∈ carrier R" shows "is_root [ 𝟭, ⊖ a ] b ⟷ a = b"
  using assms minus_equality r_neg[OF assms] unfolding is_root_def by (auto, fastforce)

lemma (in field) degree_one_root_condition:
  assumes "p ∈ carrier (poly_ring R)" and "degree p = 1"
  shows "is_root p x ⟷ x = ⊖ (inv (lead_coeff p) ⊗ (const_term p))"
proof -
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  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 list.exhaust nat.inject)
  hence a: "a ∈ carrier R" "a ≠ 𝟬" and b: "b ∈ carrier R"
    using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  hence inv_a: "inv a ∈ carrier R" "(inv a) ⊗ a = 𝟭"
    using subfield_m_inv[OF carrier_is_subfield, of a] by auto
  hence in_carrier: "[ 𝟭, (inv a) ⊗ b ] ∈ carrier (poly_ring R)"
    using b unfolding sym[OF univ_poly_carrier] polynomial_def by auto

  have "p ∼⇘poly_ring R⇙ [ 𝟭, (inv a) ⊗ b ]"
  proof (rule UP.associatedI2'[OF _ _ in_carrier, of _ "[ a ]"])
    have "p = [ a ] ⊗⇘poly_ring R⇙ [ 𝟭, inv a ⊗ b ]"
      using a inv_a b m_assoc[of a "inv a" b] unfolding p univ_poly_mult by (auto, algebra)
    also have " ... = [ 𝟭, inv a ⊗ b ] ⊗⇘poly_ring R⇙ [ a ]"
      using UP.m_comm[OF in_carrier, of "[ a ]"] a
      by (auto simp add: sym[OF univ_poly_carrier] polynomial_def)
    finally show "p = [ 𝟭, inv a ⊗ b ] ⊗⇘poly_ring R⇙ [ a ]" .
  next
    from ‹a ∈ carrier R› and ‹a ≠ 𝟬› show "[ a ] ∈ Units (poly_ring R)"
      unfolding univ_poly_units[OF carrier_is_subfield] by simp
  qed

  moreover have "(inv a) ⊗ b = ⊖ (⊖ (inv (lead_coeff p) ⊗ (const_term p)))"
    and "inv (lead_coeff p) ⊗ (const_term p) ∈ carrier R"
    using inv_a a b unfolding p const_term_def by auto

  ultimately show ?thesis
    using associated_polynomials_imp_same_is_root[OF assms(1) in_carrier]
          monic_degree_one_root_condition
    by (metis add.inv_closed)
qed

lemma (in domain) is_root_poly_mult_imp_is_root:
  assumes "p ∈ carrier (poly_ring R)" and "q ∈ carrier (poly_ring R)"
  shows "is_root (p ⊗⇘poly_ring R⇙ q) x ⟹ (is_root p x) ∨ (is_root q x)"
proof -
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  assume is_root: "is_root (p ⊗⇘poly_ring R⇙ q) x"
  hence "p ≠ []" and "q ≠ []"
    unfolding is_root_def sym[OF univ_poly_zero[of R "carrier R"]]
    using UP.l_null[OF assms(2)] UP.r_null[OF assms(1)] by blast+
  moreover have x: "x ∈ carrier R" and "eval (p ⊗⇘poly_ring R⇙ q) x = 𝟬"
    using is_root unfolding is_root_def by simp+
  hence "eval p x = 𝟬 ∨ eval q x = 𝟬"
    using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring], of x] assms integral by auto 
  ultimately show "(is_root p x) ∨ (is_root q x)"
    using x unfolding is_root_def by auto
qed

lemma (in domain) degree_zero_imp_not_is_root:
  assumes "p ∈ carrier (poly_ring R)" and "degree p = 0" shows "¬ is_root p x"
proof (cases "p = []", simp add: is_root_def)
  case False with ‹degree p = 0› have "length p = Suc 0"
    using le_SucE by fastforce 
  then obtain a where "p = [ a ]" and "a ∈ carrier R" and "a ≠ 𝟬"
    using assms unfolding sym[OF univ_poly_carrier] polynomial_def
    by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
  thus ?thesis
    unfolding is_root_def by auto 
qed

lemma (in domain) finite_number_of_roots:
  assumes "p ∈ carrier (poly_ring R)" shows "finite { x. is_root p x }"
  using assms
proof (induction "degree p" arbitrary: p)
  case 0 thus ?case
    by (simp add: degree_zero_imp_not_is_root)
next
  case (Suc n) show ?case
  proof (cases "{ x. is_root p x } = {}")
    case True thus ?thesis
      by (simp add: True) 
  next
    interpret UP: domain "poly_ring R"
      using univ_poly_is_domain[OF carrier_is_subring] .

    case False
    then obtain a where is_root: "is_root p a"
      by blast
    hence a: "a ∈ carrier R" and eval: "eval p a = 𝟬" and p_not_zero: "p ≠ []"
      unfolding is_root_def by auto
    hence in_carrier: "[ 𝟭, ⊖ a ] ∈ carrier (poly_ring R)"
      unfolding sym[OF univ_poly_carrier] polynomial_def by auto

    obtain q where q: "q ∈ carrier (poly_ring R)" and p: "p = [ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ q"
      using is_root_imp_pdivides[OF Suc(3) is_root] unfolding pdivides_def by auto
    with ‹p ≠ []› have q_not_zero: "q ≠ []"
      using UP.r_null UP.integral in_carrier unfolding sym[OF univ_poly_zero[of R "carrier R"]]
      by metis
    hence "degree q = n"
      using poly_mult_degree_eq[OF carrier_is_subring, of "[ 𝟭, ⊖ a ]" q]
            in_carrier q p_not_zero p Suc(2)
      unfolding univ_poly_carrier
      by (metis One_nat_def Suc_eq_plus1 diff_Suc_1 list.distinct(1)
                list.size(3-4) plus_1_eq_Suc univ_poly_mult)
    hence "finite { x. is_root q x }"
      using Suc(1)[OF _ q] by simp

    moreover have "{ x. is_root p x } ⊆ insert a { x. is_root q x }"
      using is_root_poly_mult_imp_is_root[OF in_carrier q]
            monic_degree_one_root_condition[OF a]
      unfolding p by auto

    ultimately show ?thesis
      using finite_subset by auto
  qed
qed

lemma (in domain) alg_multE:
  assumes "x ∈ carrier R" and "p ∈ carrier (poly_ring R)" and "p ≠ []"
  shows "([ 𝟭, ⊖ x ] [^]⇘poly_ring R⇙ (alg_mult p x)) pdivides p"
    and "⋀n. ([ 𝟭, ⊖ x ] [^]⇘poly_ring R⇙ n) pdivides p ⟹ n ≤ alg_mult p x"
proof -
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  let ?ppow = "λn :: nat. ([ 𝟭, ⊖ x ] [^]⇘poly_ring R⇙ n)"

  define S :: "nat set" where "S = { n. ?ppow n pdivides p }"
  have "?ppow 0 = 𝟭⇘poly_ring R⇙"
    using UP.nat_pow_0 by simp
  hence "0 ∈ S"
    using UP.one_divides[OF assms(2)] unfolding S_def pdivides_def by simp
  hence "S ≠ {}"
    by auto

  moreover have "n ≤ degree p" if "n ∈ S" for n :: nat
  proof -
    have "[ 𝟭, ⊖ x ] ∈ carrier (poly_ring R)"
      using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
    hence "?ppow n ∈ carrier (poly_ring R)"
      using assms unfolding univ_poly_zero by auto
    with ‹n ∈ S› have "degree (?ppow n) ≤ degree p"
      using pdivides_imp_degree_le[OF carrier_is_subring _ assms(2-3), of "?ppow n"] by (simp add: S_def)
    with ‹[ 𝟭, ⊖ x ] ∈ carrier (poly_ring R)› show ?thesis
      using polynomial_pow_degree by simp
  qed
  hence "finite S"
    using finite_nat_set_iff_bounded_le by blast

  ultimately have MaxS: "⋀n. n ∈ S ⟹ n ≤ Max S" "Max S ∈ S"
    using Max_ge[of S] Max_in[of S] by auto
  with ‹x ∈ carrier R› have "alg_mult p x = Max S"
    using Greatest_equality[of "λn. ?ppow n pdivides p" "Max S"] assms(3)
    unfolding S_def alg_mult_def by auto
  thus "([ 𝟭, ⊖ x ] [^]⇘poly_ring R⇙ (alg_mult p x)) pdivides p"
   and "⋀n. ([ 𝟭, ⊖ x ] [^]⇘poly_ring R⇙ n) pdivides p ⟹ n ≤ alg_mult p x"
    using MaxS unfolding S_def by auto
qed

lemma (in domain) le_alg_mult_imp_pdivides:
  assumes "x ∈ carrier R" and "p ∈ carrier (poly_ring R)"
  shows "n ≤ alg_mult p x ⟹ ([ 𝟭, ⊖ x ] [^]⇘poly_ring R⇙ n) pdivides p"
proof -
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  assume le_alg_mult: "n ≤ alg_mult p x"
  have in_carrier: "[ 𝟭, ⊖ x ] ∈ carrier (poly_ring R)"
    using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  hence ppow_pdivides:
    "([ 𝟭, ⊖ x ] [^]⇘poly_ring R⇙ n) pdivides
     ([ 𝟭, ⊖ x ] [^]⇘poly_ring R⇙ (alg_mult p x))"
    using polynomial_pow_division[OF _ le_alg_mult] by simp

  show ?thesis
  proof (cases "p = []")
    case True thus ?thesis
      using in_carrier pdivides_zero[OF carrier_is_subring] by auto
  next
    case False thus ?thesis
      using ppow_pdivides UP.divides_trans UP.nat_pow_closed alg_multE(1)[OF assms] in_carrier
      unfolding pdivides_def by meson
  qed
qed

lemma (in domain) alg_mult_gt_zero_iff_is_root:
  assumes "p ∈ carrier (poly_ring R)" shows "alg_mult p x > 0 ⟷ is_root p x"
proof -
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .
  show ?thesis
  proof
    assume is_root: "is_root p x" hence x: "x ∈ carrier R" and not_zero: "p ≠ []"
      unfolding is_root_def by auto
    have "[𝟭, ⊖ x] [^]⇘poly_ring R⇙ (Suc 0) = [𝟭, ⊖ x]"
      using x unfolding univ_poly_def by auto
    thus "alg_mult p x > 0"
      using is_root_imp_pdivides[OF _ is_root] alg_multE(2)[OF x, of p "Suc 0"] not_zero assms by auto
  next
    assume gt_zero: "alg_mult p x > 0"
    hence x: "x ∈ carrier R" and not_zero: "p ≠ []"
      unfolding alg_mult_def by (cases "p = []", auto, cases "x ∈ carrier R", auto)
    hence in_carrier: "[ 𝟭, ⊖ x ] ∈ carrier (poly_ring R)"
      unfolding sym[OF univ_poly_carrier] polynomial_def by auto
    with ‹x ∈ carrier R› have "[ 𝟭, ⊖ x ] pdivides p" and "eval [ 𝟭, ⊖ x ] x = 𝟬"
      using le_alg_mult_imp_pdivides[of x p "1::nat"] gt_zero assms by (auto, algebra)
    thus "is_root p x"
      using pdivides_imp_root_sharing[OF in_carrier] not_zero x by (simp add: is_root_def)
  qed
qed

lemma (in domain) alg_mult_eq_count_roots:
  assumes "p ∈ carrier (poly_ring R)" shows "alg_mult p = count (roots p)"
  using finite_number_of_roots[OF assms]
  unfolding sym[OF alg_mult_gt_zero_iff_is_root[OF assms]]
  by (simp add: roots_def) 

lemma (in domain) roots_mem_iff_is_root:
  assumes "p ∈ carrier (poly_ring R)" shows "x ∈# roots p ⟷ is_root p x"
  using alg_mult_eq_count_roots[OF assms] count_greater_zero_iff
  unfolding roots_def sym[OF alg_mult_gt_zero_iff_is_root[OF assms]] by metis

lemma (in domain) degree_zero_imp_empty_roots:
  assumes "p ∈ carrier (poly_ring R)" and "degree p = 0" shows "roots p = {#}"
  using degree_zero_imp_not_is_root[of p] roots_mem_iff_is_root[of p] assms by auto

lemma (in domain) degree_zero_imp_splitted:
  assumes "p ∈ carrier (poly_ring R)" and "degree p = 0" shows "splitted p"
  unfolding splitted_def degree_zero_imp_empty_roots[OF assms] assms(2) by simp

lemma (in domain) roots_inclI':
  assumes "p ∈ carrier (poly_ring R)" and "⋀a. ⟦ a ∈ carrier R; p ≠ [] ⟧ ⟹ alg_mult p a ≤ count m a" 
  shows "roots p ⊆# m"
proof (intro mset_subset_eqI)
  fix a show "count (roots p) a ≤ count m a"
    using assms unfolding sym[OF alg_mult_eq_count_roots[OF assms(1)]] alg_mult_def
    by (cases "p = []", simp, cases "a ∈ carrier R", auto)
qed

lemma (in domain) roots_inclI:
  assumes "p ∈ carrier (poly_ring R)" and "q ∈ carrier (poly_ring R)" "q ≠ []"
    and "⋀a. ⟦ a ∈ carrier R; p ≠ [] ⟧ ⟹ ([ 𝟭, ⊖ a ] [^]⇘poly_ring R⇙ (alg_mult p a)) pdivides q"
  shows "roots p ⊆# roots q"
  using roots_inclI'[OF assms(1), of "roots q"] assms alg_multE(2)[OF _ assms(2-3)]
  unfolding sym[OF alg_mult_eq_count_roots[OF assms(2)]] by auto

lemma (in domain) pdivides_imp_roots_incl:
  assumes "p ∈ carrier (poly_ring R)" and "q ∈ carrier (poly_ring R)" "q ≠ []"
  shows "p pdivides q ⟹ roots p ⊆# roots q"
proof (rule roots_inclI[OF assms])
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  fix a assume "p pdivides q" and a: "a ∈ carrier R"
  hence "[ 𝟭 , ⊖ a ] ∈ carrier (poly_ring R)"
    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
  with ‹p pdivides q› show "([𝟭, ⊖ a] [^]⇘poly_ring R⇙ (alg_mult p a)) pdivides q"
    using UP.divides_trans[of _p q] le_alg_mult_imp_pdivides[OF a assms(1)]
    by (auto simp add: pdivides_def)
qed

lemma (in domain) associated_polynomials_imp_same_roots:
  assumes "p ∈ carrier (poly_ring R)" and "q ∈ carrier (poly_ring R)" and "p ∼⇘poly_ring R⇙ q"
  shows "roots p = roots q"
  using assms pdivides_imp_roots_incl zero_pdivides
  unfolding pdivides_def associated_def 
  by (metis subset_mset.eq_iff)

lemma (in domain) monic_degree_one_roots:
  assumes "a ∈ carrier R" shows "roots [ 𝟭 , ⊖ a ] = {# a #}"
proof -
  let ?p = "[ 𝟭 , ⊖ a ]"

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

  from ‹a ∈ carrier R› have in_carrier: "?p ∈ carrier (poly_ring R)"
    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
  show ?thesis
  proof (rule subset_mset.antisym)
    show "{# a #} ⊆# roots ?p"
      using roots_mem_iff_is_root[OF in_carrier]
            monic_degree_one_root_condition[OF assms]
      by simp
  next
    show "roots ?p ⊆# {# a #}"
    proof (rule mset_subset_eqI, auto)
      fix b assume "a ≠ b" thus "count (roots ?p) b = 0"
        using alg_mult_gt_zero_iff_is_root[OF in_carrier]
              monic_degree_one_root_condition[OF assms]
        unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
        by fastforce
    next
      have "(?p [^]⇘poly_ring R⇙ (alg_mult ?p a)) pdivides ?p"
        using le_alg_mult_imp_pdivides[OF assms in_carrier] by simp
      hence "degree (?p [^]⇘poly_ring R⇙ (alg_mult ?p a)) ≤ degree ?p"
        using pdivides_imp_degree_le[OF carrier_is_subring, of _ ?p] in_carrier by auto
      thus "count (roots ?p) a ≤ Suc 0"
        using polynomial_pow_degree[OF in_carrier]
        unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
        by auto
    qed
  qed
qed

lemma (in domain) degree_one_roots:
  assumes "a ∈ carrier R" "a' ∈ carrier R" and "b ∈ carrier R" and "a ⊗ a' = 𝟭"
  shows "roots [ a , b ] = {# ⊖ (a' ⊗ b) #}"
proof -
  have "[ a, b ] ∈ carrier (poly_ring R)" and "[ 𝟭, a' ⊗ b ] ∈ carrier (poly_ring R)"
    using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  thus ?thesis
    using subring_degree_one_associatedI[OF carrier_is_subring assms] assms
          monic_degree_one_roots associated_polynomials_imp_same_roots
    by (metis add.inv_closed local.minus_minus m_closed)
qed

lemma (in field) degree_one_imp_singleton_roots:
  assumes "p ∈ carrier (poly_ring R)" and "degree p = 1"
  shows "roots p = {# ⊖ (inv (lead_coeff p) ⊗ (const_term p)) #}"
proof -
  from ‹p ∈ carrier (poly_ring R)› and ‹degree p = 1›
  obtain a b where "p = [ a, b ]" and "a ∈ carrier R" "a ≠ 𝟬" and "b ∈ carrier R"
    by auto
  thus ?thesis
    using degree_one_roots[of a "inv a" b]
    by (auto simp add: const_term_def field_Units)
qed

lemma (in field) degree_one_imp_splitted:
  assumes "p ∈ carrier (poly_ring R)" and "degree p = 1" shows "splitted p"
  using degree_one_imp_singleton_roots[OF assms] assms(2) unfolding splitted_def by simp

lemma (in field) no_roots_imp_same_roots:
  assumes "p ∈ carrier (poly_ring R)" "p ≠ []" and "q ∈ carrier (poly_ring R)"
  shows "roots p = {#} ⟹ roots (p ⊗⇘poly_ring R⇙ q) = roots q"
proof -
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  assume no_roots: "roots p = {#}" show "roots (p ⊗⇘poly_ring R⇙ q) = roots q"
  proof (intro subset_mset.antisym)
    have pdiv: "q pdivides (p ⊗⇘poly_ring R⇙ q)"
      using UP.divides_prod_l assms unfolding pdivides_def by blast
    show "roots q ⊆# roots (p ⊗⇘poly_ring R⇙ q)"
      using pdivides_imp_roots_incl[OF _ _ _ pdiv] assms
            degree_zero_imp_empty_roots[OF assms(3)]
      by (cases "q = []", auto, metis UP.l_null UP.m_rcancel UP.zero_closed univ_poly_zero)
  next
    show "roots (p ⊗⇘poly_ring R⇙ q) ⊆# roots q"
    proof (cases "p ⊗⇘poly_ring R⇙ q = []")
      case True thus ?thesis
        using degree_zero_imp_empty_roots[OF UP.m_closed[OF assms(1,3)]] by simp
    next
      case False with ‹p ≠ []› have q_not_zero: "q ≠ []"
        by (metis UP.r_null assms(1) univ_poly_zero)
      show ?thesis
      proof (rule roots_inclI[OF UP.m_closed[OF assms(1,3)] assms(3) q_not_zero])
        fix a assume a: "a ∈ carrier R"
        hence "¬ ([ 𝟭, ⊖ a ] pdivides p)"
          using assms(1-2) no_roots pdivides_imp_is_root roots_mem_iff_is_root[of p] by auto
        moreover have in_carrier: "[ 𝟭, ⊖ a ] ∈ carrier (poly_ring R)"
          using a unfolding sym[OF univ_poly_carrier] polynomial_def by auto
        hence "pirreducible (carrier R) [ 𝟭, ⊖ a ]"
          using degree_one_imp_pirreducible[OF carrier_is_subfield] by simp
        moreover
        have "([ 𝟭, ⊖ a ] [^]⇘poly_ring R⇙ (alg_mult (p ⊗⇘poly_ring R⇙ q) a)) pdivides (p ⊗⇘poly_ring R⇙ q)"
          using le_alg_mult_imp_pdivides[OF a UP.m_closed, of p q] assms by simp
        ultimately show "([ 𝟭, ⊖ a ] [^]⇘poly_ring R⇙ (alg_mult (p ⊗⇘poly_ring R⇙ q) a)) pdivides q"
          using pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier] assms by auto
      qed
    qed
  qed
qed

lemma (in field) poly_mult_degree_one_monic_imp_same_roots:
  assumes "a ∈ carrier R" and "p ∈ carrier (poly_ring R)" "p ≠ []"
  shows "roots ([ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ p) = add_mset a (roots p)"
proof -
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .
  
  from ‹a ∈ carrier R› have in_carrier: "[ 𝟭, ⊖ a ] ∈ carrier (poly_ring R)"
    unfolding sym[OF univ_poly_carrier] polynomial_def by simp

  show ?thesis
  proof (intro subset_mset.antisym[OF roots_inclI' mset_subset_eqI])
    show "([ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ p) ∈ carrier (poly_ring R)"
      using in_carrier assms(2) by simp
  next
    fix b assume b: "b ∈ carrier R" and "[ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ p ≠ []"
    hence not_zero: "p ≠ []"
      unfolding univ_poly_def by auto
    from ‹b ∈ carrier R› have in_carrier':  "[ 𝟭, ⊖ b ] ∈ carrier (poly_ring R)"
      unfolding sym[OF univ_poly_carrier] polynomial_def by simp
    show "alg_mult ([ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ p) b ≤ count (add_mset a (roots p)) b"
    proof (cases "a = b")
      case False
      hence "¬ [ 𝟭, ⊖ b ] pdivides [ 𝟭, ⊖ a ]"
        using assms(1) b monic_degree_one_root_condition pdivides_imp_is_root by blast
      moreover have "pirreducible (carrier R) [ 𝟭, ⊖ b ]"
        using degree_one_imp_pirreducible[OF carrier_is_subfield in_carrier'] by simp
      ultimately
      have "[ 𝟭, ⊖ b ] [^]⇘poly_ring R⇙ (alg_mult ([ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ p) b) pdivides p"
        using le_alg_mult_imp_pdivides[OF b UP.m_closed, of _ p] assms(2) in_carrier
              pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier' in_carrier, of p]
        by auto
      with ‹a ≠ b› show ?thesis
        using alg_mult_eq_count_roots[OF assms(2)] alg_multE(2)[OF b assms(2) not_zero] by auto
    next
      case True
      have "[ 𝟭, ⊖ a ] pdivides ([ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ p)"
        using dividesI[OF assms(2)] unfolding pdivides_def by auto
      with ‹[ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ p ≠ []›
      have "alg_mult ([ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ p) a ≥ Suc 0"
        using alg_multE(2)[of a _ "Suc 0"] in_carrier assms by auto
      then obtain m where m: "alg_mult ([ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ p) a = Suc m"
        using Suc_le_D by blast
      hence "([ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ ([ 𝟭, ⊖ a ] [^]⇘poly_ring R⇙ m)) pdivides
             ([ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ p)"
        using le_alg_mult_imp_pdivides[OF _ UP.m_closed, of a _ p]
              in_carrier assms UP.nat_pow_Suc2 by force
      hence "([ 𝟭, ⊖ a ] [^]⇘poly_ring R⇙ m) pdivides p"
        using UP.mult_divides in_carrier assms(2)
        unfolding univ_poly_zero pdivides_def factor_def
        by (simp add: UP.m_assoc UP.m_lcancel univ_poly_zero)
      with ‹a = b› show ?thesis
        using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2 
              alg_multE(2)[OF assms(1) _ not_zero] m
        by auto
    qed
  next
    fix b
    have not_zero: "[ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ p ≠ []"
      using assms in_carrier univ_poly_zero[of R] UP.integral by auto

    show "count (add_mset a (roots p)) b ≤ count (roots ([𝟭, ⊖ a] ⊗⇘poly_ring R⇙ p)) b"
    proof (cases "a = b")
      case True
      have "([ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ ([ 𝟭, ⊖ a ] [^]⇘poly_ring R⇙ (alg_mult p a))) pdivides
            ([ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ p)"
        using UP.divides_mult[OF _ in_carrier] le_alg_mult_imp_pdivides[OF assms(1,2)] in_carrier assms
        by (auto simp add: pdivides_def)
      with ‹a = b› show ?thesis
        using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2 
              alg_multE(2)[OF assms(1) _ not_zero]
        by auto
    next
      case False
      have "p pdivides ([ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ p)"
        using dividesI[OF in_carrier] UP.m_comm in_carrier assms unfolding pdivides_def by auto
      thus ?thesis
        using False pdivides_imp_roots_incl assms in_carrier not_zero
        by (simp add: subseteq_mset_def)
    qed
  qed
qed

lemma (in domain) not_empty_rootsE[elim]:
  assumes "p ∈ carrier (poly_ring R)" and "roots p ≠ {#}"
    and "⋀a. ⟦ a ∈ carrier R; a ∈# roots p;
               [ 𝟭, ⊖ a ] ∈ carrier (poly_ring R); [ 𝟭, ⊖ a ] pdivides p ⟧ ⟹ P"
  shows P
proof -
  from ‹roots p ≠ {#}› obtain a where "a ∈# roots p"
    by blast
  with ‹p ∈ carrier (poly_ring R)› have "[ 𝟭, ⊖ a ] pdivides p"
    and "[ 𝟭, ⊖ a ] ∈ carrier (poly_ring R)" and "a ∈ carrier R"
    using is_root_imp_pdivides[of p] roots_mem_iff_is_root[of p] is_root_def[of p a]
    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  with ‹a ∈# roots p› show ?thesis
    using assms(3)[of a] by auto
qed

lemma (in field) associated_polynomials_imp_same_roots:
  assumes "p ∈ carrier (poly_ring R)" "p ≠ []" and "q ∈ carrier (poly_ring R)" "q ≠ []"
  shows "roots (p ⊗⇘poly_ring R⇙ q) = roots p + roots q"
proof -
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .
  from assms show ?thesis
  proof (induction "degree p" arbitrary: p rule: less_induct)
    case less show ?case
    proof (cases "roots p = {#}")
      case True thus ?thesis
        using no_roots_imp_same_roots[of p q] less by simp
    next
      case False with ‹p ∈ carrier (poly_ring R)›
      obtain a where a: "a ∈ carrier R" and "a ∈# roots p" and pdiv: "[ 𝟭, ⊖ a ] pdivides p"
          and in_carrier: "[ 𝟭, ⊖ a ] ∈ carrier (poly_ring R)"
        by blast
      show ?thesis
      proof (cases "degree p = 1")
        case True with ‹p ∈ carrier (poly_ring R)›
        obtain b c where p: "p = [ b, c ]" and b: "b ∈ carrier R" "b ≠ 𝟬" and c: "c ∈ carrier R"
          by auto
        with ‹a ∈# roots p› have roots: "roots p = {# a #}" and a: "⊖ a = inv b ⊗ c" "a ∈ carrier R"
          and lead: "lead_coeff p = b" and const: "const_term p = c"
          using degree_one_imp_singleton_roots[of p] less(2) field_Units
          unfolding const_term_def by auto
        hence "(p ⊗⇘poly_ring R⇙ q) ∼⇘poly_ring R⇙ ([ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ q)"
          using UP.mult_cong_l[OF degree_one_associatedI[OF carrier_is_subfield _ True]] less(2,4)
          by (auto simp add: a lead const)
        hence "roots (p ⊗⇘poly_ring R⇙ q) = roots ([ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ q)"
          using associated_polynomials_imp_same_roots in_carrier less(2,4) unfolding a by simp
        thus ?thesis
          unfolding poly_mult_degree_one_monic_imp_same_roots[OF a(2) less(4,5)] roots by simp
      next
        case False
        from ‹[ 𝟭, ⊖ a ] pdivides p›
        obtain r where p: "p = [ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ r" and r: "r ∈ carrier (poly_ring R)"
          unfolding pdivides_def by auto
        with ‹p ≠ []› have not_zero: "r ≠ []"
          using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff by auto
        with ‹p = [ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ r› have deg: "degree p = Suc (degree r)"
          using poly_mult_degree_eq[OF carrier_is_subring, of _ r] in_carrier r
          unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
        with ‹r ≠ []› and ‹q ≠ []› have "r ⊗⇘poly_ring R⇙ q ≠ []"
          using in_carrier univ_poly_zero[of R "carrier R"] UP.integral less(4) r by auto
        hence "roots (p ⊗⇘poly_ring R⇙ q) = add_mset a (roots (r ⊗⇘poly_ring R⇙ q))"
          using poly_mult_degree_one_monic_imp_same_roots[OF a UP.m_closed[OF r less(4)]]
                UP.m_assoc[OF in_carrier r less(4)] p by auto
        also have " ... = add_mset a (roots r + roots q)"
          using less(1)[OF _ r not_zero less(4-5)] deg by simp
        also have " ... = (add_mset a (roots r)) + roots q"
          by simp
        also have " ... = roots p + roots q"
          using poly_mult_degree_one_monic_imp_same_roots[OF a r not_zero] p by simp 
        finally show ?thesis .
      qed
    qed
  qed
qed

lemma (in field) size_roots_le_degree:
  assumes "p ∈ carrier (poly_ring R)" shows "size (roots p) ≤ degree p"
  using assms
proof (induction "degree p" arbitrary: p rule: less_induct)
  case less show ?case
  proof (cases "roots p = {#}", simp)
    interpret UP: domain "poly_ring R"
      using univ_poly_is_domain[OF carrier_is_subring] .

    case False with ‹p ∈ carrier (poly_ring R)›
    obtain a where a: "a ∈ carrier R" and "a ∈# roots p" and "[ 𝟭, ⊖ a ] pdivides p"
      and in_carrier: "[ 𝟭, ⊖ a ] ∈ carrier (poly_ring R)"
      by blast
    then obtain q where p: "p = [ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ q" and q: "q ∈ carrier (poly_ring R)"
      unfolding pdivides_def by auto
    with ‹a ∈# roots p› have "p ≠ []"
      using degree_zero_imp_empty_roots[OF less(2)] by auto
    hence not_zero: "q ≠ []"
      using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff p by auto
    hence "degree p = Suc (degree q)"
      using poly_mult_degree_eq[OF carrier_is_subring, of _ q] in_carrier p q
      unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
    with ‹q ≠ []› show ?thesis
      using poly_mult_degree_one_monic_imp_same_roots[OF a q] p less(1)[OF _ q]
      by (metis Suc_le_mono lessI size_add_mset) 
  qed
qed

lemma (in domain) pirreducible_roots:
  assumes "p ∈ carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p ≠ 1"
  shows "roots p = {#}"
proof (rule ccontr)
  assume "roots p ≠ {#}" with ‹p ∈ carrier (poly_ring R)›
  obtain a where a: "a ∈ carrier R" and "a ∈# roots p" and "[ 𝟭, ⊖ a ] pdivides p"
    and in_carrier: "[ 𝟭, ⊖ a ] ∈ carrier (poly_ring R)"
    by blast
  hence "[ 𝟭, ⊖ a ] ∼⇘poly_ring R⇙ p"
    using divides_pirreducible_condition[OF assms(2) in_carrier]
          univ_poly_units_incl[OF carrier_is_subring]
    unfolding pdivides_def by auto
  hence "degree p = 1"
    using associated_polynomials_imp_same_length[OF carrier_is_subring in_carrier assms(1)] by auto
  with ‹degree p ≠ 1› show False ..
qed

lemma (in field) pirreducible_imp_not_splitted:
  assumes "p ∈ carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p ≠ 1"
  shows "¬ splitted p"
  using pirreducible_roots[of p] pirreducible_degree[OF carrier_is_subfield, of p] assms
  by (simp add: splitted_def)

lemma (in field)
  assumes "p ∈ carrier (poly_ring R)" and "q ∈ carrier (poly_ring R)"
    and "pirreducible (carrier R) p" and "degree p ≠ 1"
  shows "roots (p ⊗⇘poly_ring R⇙ q) = roots q"
  using no_roots_imp_same_roots[of p q] pirreducible_roots[of p] assms
  unfolding ring_irreducible_def univ_poly_zero by auto

lemma (in field) trivial_factors_imp_splitted:
  assumes "p ∈ carrier (poly_ring R)"
    and "⋀q. ⟦ q ∈ carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p ⟧ ⟹ degree q ≤ 1"
  shows "splitted p"
  using assms
proof (induction "degree p" arbitrary: p rule: less_induct)
  interpret UP: principal_domain "poly_ring R"
    using univ_poly_is_principal[OF carrier_is_subfield] .
  case less show ?case
  proof (cases "degree p = 0", simp add: degree_zero_imp_splitted[OF less(2)])
    case False show ?thesis
    proof (cases "roots p = {#}")
      case True
      from ‹degree p ≠ 0› have "p ∉ Units (poly_ring R)" and "p ∈ carrier (poly_ring R) - { [] }"
        using univ_poly_units'[OF carrier_is_subfield, of p] less(2) by auto
      then obtain q where "q ∈ carrier (poly_ring R)" "pirreducible (carrier R) q" and "q pdivides p"
        using UP.exists_irreducible_divisor[of p] unfolding univ_poly_zero pdivides_def by auto
      with ‹degree p ≠ 0› have "roots p ≠ {#}"
        using degree_one_imp_singleton_roots[OF _ , of q] less(3)[of q]
              pdivides_imp_roots_incl[OF _ less(2), of q]
              pirreducible_degree[OF carrier_is_subfield, of q]
        by force
      from ‹roots p = {#}› and ‹roots p ≠ {#}› have False
        by simp
      thus ?thesis ..
    next
      case False with ‹p ∈ carrier (poly_ring R)›
      obtain a where a: "a ∈ carrier R" and "a ∈# roots p" and "[ 𝟭, ⊖ a ] pdivides p"
        and in_carrier: "[ 𝟭, ⊖ a ] ∈ carrier (poly_ring R)"
        by blast
      then obtain q where p: "p = [ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ q" and q: "q ∈ carrier (poly_ring R)"
        unfolding pdivides_def by blast
      with ‹degree p ≠ 0› have "p ≠ []"
        by auto
      with ‹p = [ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ q› have "q ≠ []"
        using in_carrier q unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
      with ‹p = [ 𝟭, ⊖ a ] ⊗⇘poly_ring R⇙ q› and ‹p ≠ []› have "degree p = Suc (degree q)"
        using poly_mult_degree_eq[OF carrier_is_subring] in_carrier q
        unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
      moreover have "q pdivides p"
        using p dividesI[OF in_carrier] UP.m_comm[OF in_carrier q] by (auto simp add: pdivides_def)
      hence "degree r = 1" if "r ∈ carrier (poly_ring R)" and "pirreducible (carrier R) r"
        and "r pdivides q" for r
        using less(3)[OF that(1-2)] UP.divides_trans[OF _ _ that(1), of q p] that(3)
              pirreducible_degree[OF carrier_is_subfield that(1-2)] 
        by (auto simp add: pdivides_def)
      ultimately have "splitted q"
        using less(1)[OF _ q] by auto
      with ‹degree p = Suc (degree q)› and ‹q ≠ []› show ?thesis
        using poly_mult_degree_one_monic_imp_same_roots[OF a q]
        unfolding sym[OF p] splitted_def
        by simp
    qed
  qed
qed

lemma (in field) pdivides_imp_splitted:
  assumes "p ∈ carrier (poly_ring R)" and "q ∈ carrier (poly_ring R)" "q ≠ []" and "splitted q" 
  shows "p pdivides q ⟹ splitted p"
proof (cases "p = []")
  case True thus ?thesis
    using degree_zero_imp_splitted[OF assms(1)] by simp
next
  interpret UP: principal_domain "poly_ring R"
    using univ_poly_is_principal[OF carrier_is_subfield] .

  case False
  assume "p pdivides q"
  then obtain b where b: "b ∈ carrier (poly_ring R)" and q: "q = p ⊗⇘poly_ring R⇙ b"
    unfolding pdivides_def by auto
  with ‹q ≠ []› have "p ≠ []" and "b ≠ []"
    using assms UP.integral_iff[of p b] unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
  hence "degree p + degree b = size (roots p) + size (roots b)"
    using associated_polynomials_imp_same_roots[of p b] assms b q splitted_def
          poly_mult_degree_eq[OF carrier_is_subring,of p b]
    unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]]
    by auto
  moreover have "size (roots p) ≤ degree p" and "size (roots b) ≤ degree b"
    using size_roots_le_degree assms(1) b by auto
  ultimately show ?thesis
    unfolding splitted_def by linarith
qed

lemma (in field) splitted_imp_trivial_factors:
  assumes "p ∈ carrier (poly_ring R)" "p ≠ []" and "splitted p"
  shows "⋀q. ⟦ q ∈ carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p ⟧ ⟹ degree q = 1"
  using pdivides_imp_splitted[OF _ assms] pirreducible_imp_not_splitted
  by auto 


subsection ‹Link between @{term ‹(pmod)›} and @{term rupture_surj}›

lemma (in domain) rupture_surj_composed_with_pmod:
  assumes "subfield K R" and "p ∈ carrier (K[X])" and "q ∈ carrier (K[X])"
  shows "rupture_surj K p q = rupture_surj K p (q pmod p)"
proof -
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .
  interpret Rupt: ring "Rupt K p"
    using assms by (simp add: UP.cgenideal_ideal ideal.quotient_is_ring rupture_def)

  let ?h = "rupture_surj K p"

  have "?h q = (?h p ⊗⇘Rupt K p⇙ ?h (q pdiv p)) ⊕⇘Rupt K p⇙ ?h (q pmod p)"
   and "?h (q pdiv p) ∈ carrier (Rupt K p)" "?h (q pmod p) ∈ carrier (Rupt K p)"
    using pdiv_pmod[OF assms(1,3,2)] long_division_closed[OF assms(1,3,2)] assms UP.m_closed
          ring_hom_memE[OF rupture_surj_hom(1)[OF subfieldE(1)[OF assms(1)] assms(2)]]
    by metis+
  moreover have "?h p = PIdl⇘K[X]⇙ p"
    using assms by (simp add: UP.a_rcos_zero UP.cgenideal_ideal UP.cgenideal_self)
  hence "?h p = 𝟬⇘Rupt K p⇙"
    unfolding rupture_def FactRing_def by simp
  ultimately show ?thesis
    by simp
qed

corollary (in domain) rupture_carrier_as_pmod_image:
  assumes "subfield K R" and "p ∈ carrier (K[X])"
  shows "(rupture_surj K p) ` ((λq. q pmod p) ` (carrier (K[X]))) = carrier (Rupt K p)"
    (is "?lhs = ?rhs")
proof
  have "(λq. q pmod p) ` carrier (K[X]) ⊆ carrier (K[X])"
    using long_division_closed(2)[OF assms(1) _ assms(2)] by auto
  thus "?lhs ⊆ ?rhs"
    using ring_hom_memE(1)[OF rupture_surj_hom(1)[OF subfieldE(1)[OF assms(1)] assms(2)]] by auto
next
  show "?rhs ⊆ ?lhs"
  proof
    fix a assume "a ∈ carrier (Rupt K p)"
    then obtain q where "q ∈ carrier (K[X])" and "a = rupture_surj K p q"
      unfolding rupture_def FactRing_def A_RCOSETS_def' by auto
    thus "a ∈ ?lhs"
      using rupture_surj_composed_with_pmod[OF assms] by auto
  qed
qed

lemma (in domain) rupture_surj_inj_on:
  assumes "subfield K R" and "p ∈ carrier (K[X])"
  shows "inj_on (rupture_surj K p) ((λq. q pmod p) ` (carrier (K[X])))"
proof (intro inj_onI)
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .

  fix a b
  assume "a ∈ (λq. q pmod p) ` carrier (K[X])"
     and "b ∈ (λq. q pmod p) ` carrier (K[X])"
  then obtain q s
    where q: "q ∈ carrier (K[X])" "a = q pmod p"
      and s: "s ∈ carrier (K[X])" "b = s pmod p"
    by auto
  moreover assume "rupture_surj K p a = rupture_surj K p b"
  ultimately have "q ⊖⇘K[X]⇙ s ∈ (PIdl⇘K[X]⇙ p)"
    using UP.quotient_eq_iff_same_a_r_cos[OF UP.cgenideal_ideal[OF assms(2)], of q s]
          rupture_surj_composed_with_pmod[OF assms] by auto
  hence "p pdivides (q ⊖⇘K[X]⇙ s)"
    using assms q(1) s(1) UP.to_contain_is_to_divide pdivides_iff_shell
    by (meson UP.cgenideal_ideal UP.cgenideal_minimal UP.minus_closed)
  thus "a = b"
    unfolding q s same_pmod_iff_pdivides[OF assms(1) q(1) s(1) assms(2)] .
qed


subsection ‹Dimension›

definition (in ring) exp_base :: "'a ⇒ nat ⇒ 'a list"
  where "exp_base x n = map (λi. x [^] i) (rev [0..< n])"

lemma (in ring) exp_base_closed:
  assumes "x ∈ carrier R" shows "set (exp_base x n) ⊆ carrier R"
  using assms by (induct n) (auto simp add: exp_base_def)

lemma (in ring) exp_base_append:
  shows "exp_base x (n + m) = (map (λi. x [^] i) (rev [n..< n + m])) @ exp_base x n"
  unfolding exp_base_def by (metis map_append rev_append upt_add_eq_append zero_le)

lemma (in ring) drop_exp_base:
  shows "drop n (exp_base x m) = exp_base x (m - n)"
proof -
  have ?thesis if "n > m"
    using that by (simp add: exp_base_def)
  moreover have ?thesis if "n ≤ m"
    using exp_base_append[of x "m - n" n] that by auto
  ultimately show ?thesis
    by linarith 
qed

lemma (in ring) combine_eq_eval:
  shows "combine Ks (exp_base x (length Ks)) = eval Ks x"
  unfolding exp_base_def by (induct Ks) (auto)

lemma (in domain) pmod_image_characterization:
  assumes "subfield K R" and "p ∈ carrier (K[X])" and "p ≠ []"
  shows "(λq. q pmod p) ` carrier (K[X]) = { q ∈ carrier (K[X]). length q ≤ degree p }"
proof -
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .

  show ?thesis
  proof (rule order_antisym; rule subsetI)
    fix q assume "q ∈ { q ∈ carrier (K[X]). length q ≤ degree p }"
    then have "q ∈ carrier (K[X])" and "length q ≤ degree p"
      by simp+

    show "q ∈ (λq. q pmod p) ` carrier (K[X])"
    proof (cases "q = []")
      case True
      have "p pmod p = q"
        unfolding True pmod_zero_iff_pdivides[OF assms(1,2,2)]
        using assms(1-2) pdivides_iff_shell by auto
      thus ?thesis
        using assms(2) by blast 
    next
      case False
      with ‹length q ≤ degree p› have "degree q < degree p"
        using le_eq_less_or_eq by fastforce 
      with ‹q ∈ carrier (K[X])› show ?thesis
        using pmod_const(2)[OF assms(1) _ assms(2), of q] by (metis imageI) 
    qed
  next
    fix q assume "q ∈ (λq. q pmod p) ` carrier (K[X])"
    then obtain q' where "q' ∈ carrier (K[X])" and "q = q' pmod p"
      by auto
    thus "q ∈ { q ∈ carrier (K[X]). length q ≤ degree p }"
      using long_division_closed(2)[OF assms(1) _ assms(2), of q']
            pmod_degree[OF assms(1) _ assms(2-3), of q']
      by auto
  qed
qed

lemma (in domain) Span_var_pow_base:
  assumes "subfield K R"
  shows "ring.Span (K[X]) (poly_of_const ` K) (ring.exp_base (K[X]) X n) =
         { q ∈ carrier (K[X]). length q ≤ n }" (is "?lhs = ?rhs")
proof -
  note subring = subfieldE(1)[OF assms]
  note subfield = univ_poly_subfield_of_consts[OF assms]

  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF subring] .

  show ?thesis
  proof (rule order_antisym; rule subsetI)
    fix q assume "q ∈ { q ∈ carrier (K[X]). length q ≤ n }"
    then have q: "q ∈ carrier (K[X])" "length q ≤ n"
      by simp+

    let ?repl = "replicate (n - length q) 𝟬⇘K[X]⇙"
    let ?map = "map poly_of_const q"
    let ?comb = "UP.combine"
    define Ks where "Ks = ?repl @ ?map"

    have "q = ?comb ?map (UP.exp_base X (length q))"
      using q eval_rewrite[OF subring q(1)] unfolding sym[OF UP.combine_eq_eval] by auto
    moreover from ‹length q ≤ n›
    have "?comb (?repl @ Ks) (UP.exp_base X n) =  ?comb Ks (UP.exp_base X (length q))"
      if "set Ks ⊆ carrier (K[X])" for Ks
      using UP.combine_prepend_replicate[OF that UP.exp_base_closed[OF var_closed(1)[OF subring]]]
      unfolding UP.drop_exp_base by auto

    moreover have "set ?map ⊆ carrier (K[X])"
      using map_norm_in_poly_ring_carrier[OF subring q(1)]
      unfolding sym[OF univ_poly_carrier] polynomial_def by auto
    
    moreover have "?repl = map poly_of_const (replicate (n - length q) 𝟬)"
      unfolding poly_of_const_def univ_poly_zero by (induct "n - length q") (auto)
    hence "set ?repl ⊆ poly_of_const ` K"
      using subringE(2)[OF subring] by auto
    moreover from ‹q ∈ carrier (K[X])› have "set q ⊆ K"
      unfolding sym[OF univ_poly_carrier] polynomial_def by auto
    hence "set ?map ⊆ poly_of_const ` K"
      by auto

    ultimately have "q = ?comb Ks (UP.exp_base X n)" and "set Ks ⊆ poly_of_const ` K"
      by (simp add: Ks_def)+
    thus "q ∈ UP.Span (poly_of_const ` K) (UP.exp_base X n)"
      using UP.Span_eq_combine_set[OF subfield UP.exp_base_closed[OF var_closed(1)[OF subring]]] by auto
  next
    fix q assume "q ∈ UP.Span (poly_of_const ` K) (UP.exp_base X n)"
    thus "q ∈ { q ∈ carrier (K[X]). length q ≤ n }"
    proof (induction n arbitrary: q)
      case 0 thus ?case
        unfolding UP.exp_base_def by (auto simp add: univ_poly_zero)
    next
      case (Suc n)
      then obtain k p where k: "k ∈ K" and p: "p ∈ UP.Span (poly_of_const ` K) (UP.exp_base X n)"
        and q: "q = ((poly_of_const k) ⊗⇘K[X]⇙ (X [^]⇘K[X]⇙ n)) ⊕⇘K[X]⇙ p"
        unfolding UP.exp_base_def using UP.line_extension_mem_iff by auto
      have p_in_carrier: "p ∈ carrier (K[X])" and "length p ≤ n"
        using Suc(1)[OF p] by simp+
      moreover from ‹k ∈ K› have "poly_of_const k ∈ carrier (K[X])"
        unfolding poly_of_const_def sym[OF univ_poly_carrier] polynomial_def by auto
      ultimately have "q ∈ carrier (K[X])"
        unfolding q using var_pow_closed[OF subring, of n] by algebra

      moreover have "poly_of_const k = 𝟬⇘K[X]⇙" if "k = 𝟬"
        unfolding poly_of_const_def that univ_poly_zero by simp
      with ‹p ∈ carrier (K[X])› have "q = p" if "k = 𝟬"
        unfolding q using var_pow_closed[OF subring, of n] that by algebra
      with ‹length p ≤ n› have "length q ≤ Suc n" if "k = 𝟬"
        using that by simp

      moreover have "poly_of_const k = [ k ]" if "k ≠ 𝟬"
        unfolding poly_of_const_def using that by simp
      hence monom: "monom k n = (poly_of_const k) ⊗⇘K[X]⇙ (X [^]⇘K[X]⇙ n)" if "k ≠ 𝟬"
        using that monom_eq_var_pow[OF subring] subfieldE(3)[OF assms] k by auto
      with ‹p ∈ carrier (K[X])› and ‹k ∈ K› and ‹length p ≤ n›
      have "length q = Suc n" if "k ≠ 𝟬"
        using that poly_add_length_eq[OF subring monom_is_polynomial[OF subring, of k n], of p]
        unfolding univ_poly_carrier monom_def univ_poly_add sym[OF monom[OF that]] q by auto  
      ultimately show ?case
        by (cases "k = 𝟬", auto)
    qed
  qed
qed

lemma (in domain) var_pow_base_independent:
  assumes "subfield K R"
  shows "ring.independent (K[X]) (poly_of_const ` K) (ring.exp_base (K[X]) X n)"
proof -
  note subring = subfieldE(1)[OF assms]
  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF subring] .

  show ?thesis
  proof (induction n, simp add: UP.exp_base_def)
    case (Suc n)
    have "X [^]⇘K[X]⇙ n ∉ UP.Span (poly_of_const ` K) (ring.exp_base (K[X]) X n)"
      unfolding sym[OF unitary_monom_eq_var_pow[OF subring]] monom_def
                Span_var_pow_base[OF assms] by auto
    moreover have "X [^]⇘K[X]⇙ n # UP.exp_base X n = UP.exp_base X (Suc n)"
      unfolding UP.exp_base_def by simp
    ultimately show ?case
      using UP.li_Cons[OF var_pow_closed[OF subring, of n] _Suc] by simp
  qed
qed

lemma (in domain) bounded_degree_dimension:
  assumes "subfield K R"
  shows "ring.dimension (K[X]) n (poly_of_const ` K) { q ∈ carrier (K[X]). length q ≤ n }"
proof -
  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF subfieldE(1)[OF assms]] .
  have "length (UP.exp_base X n) = n"
    unfolding UP.exp_base_def by simp
  thus ?thesis
    using UP.dimension_independent[OF var_pow_base_independent[OF assms], of n]
    unfolding Span_var_pow_base[OF assms] by simp
qed

corollary (in domain) univ_poly_infinite_dimension:
  assumes "subfield K R" shows "ring.infinite_dimension (K[X]) (poly_of_const ` K) (carrier (K[X]))"
proof (rule ccontr)
  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF subfieldE(1)[OF assms]] .

  assume "¬ UP.infinite_dimension (poly_of_const ` K) (carrier (K[X]))"
  then obtain n where n: "UP.dimension n (poly_of_const ` K) (carrier (K[X]))"
    by blast
  show False
    using UP.independent_length_le_dimension[OF univ_poly_subfield_of_consts[OF assms] n
          var_pow_base_independent[OF assms, of "Suc n"]
          UP.exp_base_closed[OF var_closed(1)[OF subfieldE(1)[OF assms]]]]
    unfolding UP.exp_base_def by simp
qed

corollary (in domain) rupture_dimension:
  assumes "subfield K R" and "p ∈ carrier (K[X])" and "degree p > 0"
  shows "ring.dimension (Rupt K p) (degree p) ((rupture_surj K p) ` poly_of_const ` K) (carrier (Rupt K p))"
proof -
  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF subfieldE(1)[OF assms(1)]] .
  interpret Hom: ring_hom_ring "K[X]" "Rupt K p" "rupture_surj K p"
    using rupture_surj_hom(2)[OF subfieldE(1)[OF assms(1)] assms(2)] .

  have not_nil: "p ≠ []"
    using assms(3) by auto

  show ?thesis
    using Hom.inj_hom_dimension[OF univ_poly_subfield_of_consts rupture_one_not_zero
          rupture_surj_inj_on] bounded_degree_dimension assms
    unfolding sym[OF rupture_carrier_as_pmod_image[OF assms(1-2)]]
              pmod_image_characterization[OF assms(1-2) not_nil]
    by simp
qed

end