# Theory 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)

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)

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 ] = [ 𝟭 ]"
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)]]
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]
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
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'"
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
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
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

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
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
proof (cases)
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
qed simp
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

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
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
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"
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)
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
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)
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 = ```