Theory Monic_Polynomial_Factorization

section ‹Factorization into Monic Polynomials\label{sec:monic}›

theory Monic_Polynomial_Factorization
imports
  Finite_Fields_Factorization_Ext
  Formal_Polynomial_Derivatives
begin

hide_const Factorial_Ring.multiplicity
hide_const Factorial_Ring.irreducible

lemma (in domain) finprod_mult_of:
  assumes "finite A"
  assumes "⋀x. x ∈ A ⟹ f x ∈ carrier (mult_of R)"
  shows "finprod R f A = finprod (mult_of R) f A"
  using assms by (induction A rule:finite_induct, auto)

lemma (in ring) finite_poly:
  assumes "subring K R"
  assumes "finite K"
  shows
    "finite {f. f ∈ carrier (K[X]) ∧ degree f = n}" (is "finite ?A")
    "finite {f. f ∈ carrier (K[X]) ∧ degree f ≤ n}" (is "finite ?B")
proof -
  have "finite {f. set f ⊆ K ∧ length f ≤ n + 1}" (is "finite ?C")
    using assms(2) finite_lists_length_le by auto
  moreover have "?B ⊆ ?C"
    by (intro subsetI)
      (auto simp:univ_poly_carrier[symmetric] polynomial_def)
  ultimately show a: "finite ?B"
    using finite_subset by auto
  moreover have "?A ⊆ ?B"
    by (intro subsetI, simp)
  ultimately show "finite ?A"
    using finite_subset by auto
qed

definition pmult :: "_ ⇒ 'a list ⇒ 'a list ⇒ nat" ("pmultı")
  where "pmult⇘R⇙ d p = multiplicity (mult_of (poly_ring R)) d p"

definition monic_poly :: "_ ⇒ 'a list ⇒ bool"
  where "monic_poly R f =
    (f ≠ [] ∧ lead_coeff f = 𝟭⇘R⇙ ∧ f ∈ carrier (poly_ring R))"

definition monic_irreducible_poly where
  "monic_irreducible_poly R f =
    (monic_poly R f ∧ pirreducible⇘R⇙ (carrier R) f)"

abbreviation "m_i_p ≡ monic_irreducible_poly"

locale polynomial_ring = field +
  fixes K
  assumes polynomial_ring_assms: "subfield K R"
begin

lemma K_subring: "subring K R"
  using polynomial_ring_assms subfieldE(1) by auto

abbreviation P where "P ≡ K[X]"

text ‹This locale is used to specialize the following lemmas for a fixed coefficient ring.
It can be introduced in a context as an intepretation to be able to use the following specialized
lemmas. Because it is not (and should not) introduced as a sublocale it has no lasting effect
for the field locale itself.›

lemmas
    poly_mult_lead_coeff = poly_mult_lead_coeff[OF K_subring]
and degree_add_distinct = degree_add_distinct[OF K_subring]
and coeff_add = coeff_add[OF K_subring]
and var_closed = var_closed[OF K_subring]
and degree_prod = degree_prod[OF _ K_subring]
and degree_pow = degree_pow[OF K_subring]
and pirreducible_degree = pirreducible_degree[OF polynomial_ring_assms]
and degree_one_imp_pirreducible =
    degree_one_imp_pirreducible[OF polynomial_ring_assms]
and var_pow_closed = var_pow_closed[OF K_subring]
and var_pow_carr = var_pow_carr[OF K_subring]
and univ_poly_a_inv_degree = univ_poly_a_inv_degree[OF K_subring]
and var_pow_degree = var_pow_degree[OF K_subring]
and pdivides_zero = pdivides_zero[OF K_subring]
and pdivides_imp_degree_le = pdivides_imp_degree_le[OF K_subring]
and var_carr = var_carr[OF K_subring]
and rupture_eq_0_iff = rupture_eq_0_iff[OF polynomial_ring_assms]
and rupture_is_field_iff_pirreducible =
    rupture_is_field_iff_pirreducible[OF polynomial_ring_assms]
and rupture_surj_hom = rupture_surj_hom[OF K_subring]
and canonical_embedding_ring_hom =
    canonical_embedding_ring_hom[OF K_subring]
and rupture_surj_norm_is_hom = rupture_surj_norm_is_hom[OF K_subring]
and rupture_surj_as_eval = rupture_surj_as_eval[OF K_subring]
and eval_cring_hom = eval_cring_hom[OF K_subring]
and coeff_range = coeff_range[OF K_subring]
and finite_poly = finite_poly[OF K_subring]
and int_embed_consistent_with_poly_of_const =
    int_embed_consistent_with_poly_of_const[OF K_subring]
and pderiv_var_pow = pderiv_var_pow[OF _ K_subring]
and pderiv_add = pderiv_add[OF K_subring]
and pderiv_inv = pderiv_inv[OF K_subring]
and pderiv_mult = pderiv_mult[OF K_subring]
and pderiv_pow = pderiv_pow[OF _ K_subring]
and pderiv_carr = pderiv_carr[OF K_subring]

sublocale p:principal_domain "poly_ring R"
  by (simp add: carrier_is_subfield univ_poly_is_principal)

end

context field
begin

interpretation polynomial_ring "R" "carrier R"
  using carrier_is_subfield field_axioms
  by (simp add:polynomial_ring_def polynomial_ring_axioms_def)

lemma pdivides_mult_r:
  assumes "a ∈ carrier (mult_of P)"
  assumes "b ∈ carrier (mult_of P)"
  assumes "c ∈ carrier (mult_of P)"
  shows "a ⊗⇘P⇙ c pdivides b ⊗⇘P⇙ c ⟷ a pdivides b"
    (is "?lhs ⟷ ?rhs")
proof -
  have a:"b ⊗⇘P⇙ c ∈ carrier P - {𝟬⇘P⇙}"
    using assms p.mult_of.m_closed by force
  have b:"a ⊗⇘P⇙ c ∈ carrier P"
    using assms by simp
  have c:"b ∈ carrier P - {𝟬⇘P⇙}"
    using assms p.mult_of.m_closed by force
  have d:"a ∈ carrier P" using assms by simp
  have "?lhs ⟷ a ⊗⇘P⇙ c divides⇘mult_of P⇙ b ⊗⇘P⇙ c"
    unfolding pdivides_def using p.divides_imp_divides_mult a b
    by (meson divides_mult_imp_divides)
  also have "... ⟷ a divides⇘mult_of P⇙ b"
    using p.mult_of.divides_mult_r[OF assms] by simp
  also have "... ⟷ ?rhs"
    unfolding pdivides_def using p.divides_imp_divides_mult c d
    by (meson divides_mult_imp_divides)
  finally show ?thesis by simp
qed

lemma lead_coeff_carr:
  assumes "x ∈ carrier (mult_of P)"
  shows "lead_coeff x ∈ carrier R - {𝟬}"
proof (cases x)
  case Nil
  then show ?thesis using assms by (simp add:univ_poly_zero)
next
  case (Cons a list)
  hence a: "polynomial (carrier R) (a # list)"
    using assms univ_poly_carrier by auto
  have "lead_coeff x = a"
    using Cons by simp
  also have "a ∈ carrier R - {𝟬}"
    using lead_coeff_not_zero a by simp
  finally show ?thesis by simp
qed

lemma lead_coeff_poly_of_const:
  assumes "r ≠ 𝟬"
  shows "lead_coeff (poly_of_const r) = r"
  using assms
  by (simp add:poly_of_const_def)

lemma lead_coeff_mult:
  assumes "f ∈ carrier (mult_of P)"
  assumes "g ∈ carrier (mult_of P)"
  shows "lead_coeff (f ⊗⇘P⇙ g) = lead_coeff f ⊗ lead_coeff g"
  unfolding univ_poly_mult using assms
  using univ_poly_carrier[where R="R" and K="carrier R"]
  by (subst poly_mult_lead_coeff) (simp_all add:univ_poly_zero)

lemma monic_poly_carr:
  assumes "monic_poly R f"
  shows "f ∈ carrier P"
  using assms unfolding monic_poly_def by simp

lemma monic_poly_add_distinct:
  assumes "monic_poly R f"
  assumes "g ∈ carrier P" "degree g < degree f"
  shows "monic_poly R (f ⊕⇘P⇙ g)"
proof (cases "g ≠ 𝟬⇘P⇙")
  case True
  define n where "n = degree f"
  have "f ∈ carrier P - {𝟬⇘P⇙}"
    using assms(1) univ_poly_zero
    unfolding monic_poly_def by auto
  hence "degree (f ⊕⇘P⇙ g) = max (degree f) (degree g)"
    using assms(2,3) True
    by (subst degree_add_distinct, simp_all)
  also have "... = degree f"
    using assms(3) by simp
  finally have b: "degree (f ⊕⇘P⇙ g) = n"
    unfolding n_def by simp
  moreover have "n > 0"
    using assms(3) unfolding n_def by simp
  ultimately have "degree (f ⊕⇘P⇙ g) ≠ degree ([])"
    by simp
  hence a:"f ⊕⇘P⇙ g ≠ []" by auto

  have "degree [] = 0" by simp
  also have  "... < degree f"
    using assms(3) by simp
  finally have "degree f ≠ degree []" by simp
  hence c: "f ≠ []" by auto

  have d: "length g ≤ n"
    using  assms(3) unfolding n_def by simp

  have "lead_coeff (f ⊕⇘P⇙ g) = coeff (f ⊕⇘P⇙ g) n"
    using a b by (cases "f ⊕⇘P⇙ g", auto)
  also have "... = coeff f n ⊕ coeff g n"
    using monic_poly_carr assms
    by (subst coeff_add, auto)
  also have "... = lead_coeff f ⊕ coeff g n"
    using c unfolding n_def by (cases "f", auto)
  also have "... = 𝟭 ⊕ 𝟬"
    using assms(1) unfolding monic_poly_def
    unfolding subst coeff_length[OF d] by simp
  also have "... = 𝟭"
    by simp
  finally have "lead_coeff (f ⊕⇘P⇙ g) = 𝟭" by simp
  moreover have "f ⊕⇘P⇙ g ∈ carrier P"
    using monic_poly_carr assms by simp
  ultimately show  ?thesis
    using a  unfolding monic_poly_def by auto
next
  case False
  then show ?thesis using assms monic_poly_carr by simp
qed

lemma monic_poly_one: "monic_poly R 𝟭⇘P⇙"
proof -
  have "𝟭⇘P⇙ ∈ carrier P"
    by simp
  thus ?thesis
    by (simp add:univ_poly_one monic_poly_def)
qed

lemma monic_poly_var: "monic_poly R X"
proof -
  have "X ∈ carrier P"
    using var_closed by simp
  thus ?thesis
    by (simp add:var_def monic_poly_def)
qed

lemma monic_poly_carr_2:
  assumes "monic_poly R f"
  shows "f ∈ carrier (mult_of P)"
  using assms unfolding monic_poly_def
  by (simp add:univ_poly_zero)

lemma monic_poly_mult:
  assumes "monic_poly R f"
  assumes "monic_poly R g"
  shows "monic_poly R (f ⊗⇘P⇙ g)"
proof -
  have "lead_coeff (f ⊗⇘P⇙ g) = lead_coeff f ⊗⇘R⇙ lead_coeff g"
    using assms monic_poly_carr_2
    by (subst lead_coeff_mult) auto
  also have "... =  𝟭"
    using assms unfolding monic_poly_def by simp
  finally have "lead_coeff (f ⊗⇘P⇙ g) = 𝟭⇘R⇙" by simp
  moreover have "(f ⊗⇘P⇙ g) ∈ carrier (mult_of P)"
    using monic_poly_carr_2 assms by blast
  ultimately show ?thesis
    by (simp add:monic_poly_def univ_poly_zero)
qed

lemma monic_poly_pow:
  assumes "monic_poly R f"
  shows "monic_poly R (f [^]⇘P⇙ (n::nat))"
  using assms monic_poly_one monic_poly_mult
  by (induction n, auto)

lemma monic_poly_prod:
  assumes "finite A"
  assumes "⋀x. x ∈ A ⟹ monic_poly R (f x)"
  shows "monic_poly R (finprod P f A)"
  using assms
proof (induction A rule:finite_induct)
  case empty
  then show ?case by (simp add:monic_poly_one)
next
  case (insert x F)
  have a: "f ∈ F → carrier P"
    using insert monic_poly_carr by simp
  have b: "f x ∈ carrier P"
    using insert monic_poly_carr by simp
  have "monic_poly R (f x ⊗⇘P⇙ finprod P f F)"
    using insert by (intro monic_poly_mult) auto
  thus ?case
    using insert a b by (subst p.finprod_insert, auto)
qed

lemma monic_poly_not_assoc:
  assumes "monic_poly R f"
  assumes "monic_poly R g"
  assumes "f ∼⇘(mult_of P)⇙ g"
  shows "f = g"
proof -
  obtain u where u_def: "f = g ⊗⇘P⇙ u" "u ∈ Units (mult_of P)"
    using p.mult_of.associatedD2 assms monic_poly_carr_2
    by blast

  hence "u ∈ Units P" by simp
  then obtain v where v_def: "u = [v]" "v ≠ 𝟬⇘R⇙" "v ∈ carrier R"
    using univ_poly_carrier_units by auto

  have "𝟭 = lead_coeff f"
    using assms(1) by (simp add:monic_poly_def)
  also have  "... = lead_coeff (g ⊗⇘P⇙ u)"
    by (simp add:u_def)
  also have "... = lead_coeff g ⊗ lead_coeff u"
    using assms(2) monic_poly_carr_2 v_def u_def(2)
    by (subst lead_coeff_mult, auto simp add:univ_poly_zero)
  also have "... = lead_coeff g ⊗ v"
    using v_def by simp
  also have "... = v"
    using assms(2) v_def(3) by (simp add:monic_poly_def)
  finally have "𝟭 = v" by simp
  hence "u = 𝟭⇘P⇙"
    using v_def by (simp add:univ_poly_one)
  thus "f = g"
    using u_def assms monic_poly_carr by simp
qed

lemma monic_poly_span:
  assumes "x ∈ carrier (mult_of P)" "irreducible (mult_of P) x"
  shows "∃y. monic_irreducible_poly R y ∧ x ∼⇘(mult_of P)⇙ y"
proof -
  define z where "z = poly_of_const (inv (lead_coeff x))"
  define y where "y = x ⊗⇘P⇙ z"

  have x_carr: "x ∈ carrier (mult_of P)" using assms by simp

  hence lx_ne_0: "lead_coeff x ≠ 𝟬"
    and lx_unit: "lead_coeff x ∈ Units R"
    using lead_coeff_carr[OF x_carr] by (auto simp add:field_Units)
  have lx_inv_ne_0: "inv (lead_coeff x) ≠ 𝟬"
    using lx_unit
    by (metis Units_closed Units_r_inv r_null zero_not_one)
  have lx_inv_carr: "inv (lead_coeff x) ∈ carrier R"
    using lx_unit by simp

  have "z ∈ carrier P"
    using lx_inv_carr poly_of_const_over_carrier
    unfolding z_def by auto
  moreover have "z ≠ 𝟬⇘P⇙"
    using lx_inv_ne_0
    by (simp add:z_def poly_of_const_def univ_poly_zero)
  ultimately have z_carr: "z ∈ carrier (mult_of P)" by simp
  have z_unit: "z ∈ Units (mult_of P)"
    using lx_inv_ne_0 lx_inv_carr
    by (simp add:univ_poly_carrier_units z_def poly_of_const_def)
  have y_exp: "y = x ⊗⇘(mult_of P)⇙ z"
    by (simp add:y_def)
  hence y_carr: "y ∈ carrier (mult_of P)"
    using x_carr z_carr p.mult_of.m_closed by simp

  have "irreducible (mult_of P) y"
    unfolding y_def using assms z_unit z_carr
    by (intro p.mult_of.irreducible_prod_rI, auto)
  moreover have "lead_coeff y = 𝟭⇘R⇙"
    unfolding y_def using x_carr z_carr lx_inv_ne_0 lx_unit
    by (simp add: lead_coeff_mult z_def lead_coeff_poly_of_const)
  hence "monic_poly R y"
    using y_carr unfolding monic_poly_def
    by (simp add:univ_poly_zero)
  ultimately have "monic_irreducible_poly R y"
    using p.irreducible_mult_imp_irreducible y_carr
    by (simp add:monic_irreducible_poly_def ring_irreducible_def)
  moreover have "y ∼⇘(mult_of P)⇙ x"
    by (intro p.mult_of.associatedI2[OF z_unit] y_def x_carr)
  hence "x ∼⇘(mult_of P)⇙ y"
    using x_carr y_carr by (simp add:p.mult_of.associated_sym)
  ultimately show ?thesis by auto
qed

lemma monic_polys_are_canonical_irreducibles:
  "canonical_irreducibles (mult_of P) {d. monic_irreducible_poly R d}"
  (is "canonical_irreducibles (mult_of P) ?S")
proof -
  have sp_1:
    "?S ⊆ {x ∈ carrier (mult_of P). irreducible (mult_of P) x}"
    unfolding monic_irreducible_poly_def ring_irreducible_def
    using monic_poly_carr
    by (intro subsetI, simp add: p.irreducible_imp_irreducible_mult)
  have sp_2: "x = y"
      if "x ∈ ?S" "y ∈ ?S" "x ∼⇘(mult_of P)⇙ y" for x y
    using that monic_poly_not_assoc
    by (simp add:monic_irreducible_poly_def)

  have sp_3: "∃y ∈ ?S. x ∼⇘(mult_of P)⇙ y"
    if "x ∈ carrier (mult_of P)" "irreducible (mult_of P) x" for x
    using that monic_poly_span by simp

  thus ?thesis using sp_1 sp_2 sp_3
    unfolding canonical_irreducibles_def by simp
qed

lemma
  assumes "monic_poly R a"
  shows factor_monic_poly:
    "a = (⨂⇘P⇙d∈{d. monic_irreducible_poly R d ∧ pmult d a > 0}.
      d [^]⇘P⇙ pmult d a)" (is "?lhs = ?rhs")
    and factor_monic_poly_fin:
      "finite {d. monic_irreducible_poly R d ∧ pmult d a > 0}"
proof -
  let ?S = "{d. monic_irreducible_poly R d}"
  let ?T = "{d. monic_irreducible_poly R d ∧ pmult d a > 0}"
  let ?mip = "monic_irreducible_poly R"

  have sp_4: "a ∈ carrier (mult_of P)"
    using assms monic_poly_carr_2
    unfolding monic_irreducible_poly_def by simp

  have b_1: "x ∈ carrier (mult_of P)" if "?mip x" for x
    using that monic_poly_carr_2
    unfolding monic_irreducible_poly_def by simp
  have b_2:"irreducible (mult_of P) x" if "?mip x" for x
    using that
    unfolding monic_irreducible_poly_def ring_irreducible_def
    by (simp add: monic_poly_carr p.irreducible_imp_irreducible_mult)
  have b_3:"x ∈ carrier P" if "?mip x" for x
    using that monic_poly_carr
    unfolding monic_irreducible_poly_def
    by simp

  have a_carr: "a ∈ carrier P - {𝟬⇘P⇙}"
    using sp_4 by simp

  have "?T = {d. ?mip d ∧ multiplicity (mult_of P) d a > 0}"
    by (simp add:pmult_def)
  also have "... = {d ∈ ?S. multiplicity (mult_of P) d a > 0}"
    using p.mult_of.multiplicity_gt_0_iff[OF b_1 b_2 sp_4]
    by (intro order_antisym subsetI, auto)
  finally have t:"?T = {d ∈ ?S. multiplicity (mult_of P) d a > 0}"
    by simp

  show fin_T: "finite ?T"
    unfolding t
    using p.mult_of.split_factors(1)
      [OF monic_polys_are_canonical_irreducibles]
    using sp_4 by auto

  have a:"x [^]⇘P⇙ (n::nat) ∈ carrier (mult_of P)" if "?mip x" for x n
  proof -
    have "monic_poly R (x [^]⇘P⇙ n)"
      using that monic_poly_pow
      unfolding monic_irreducible_poly_def by auto
    thus ?thesis
      using monic_poly_carr_2 by simp
  qed

  have "?lhs ∼⇘(mult_of P)⇙
    finprod (mult_of P)
      (λd. d [^]⇘(mult_of P)⇙ (multiplicity (mult_of P) d a)) ?T"
    unfolding t
    by (intro p.mult_of.split_factors(2)
        [OF monic_polys_are_canonical_irreducibles sp_4])
  also have "... =
    finprod (mult_of P) (λd. d [^]⇘P⇙ (multiplicity (mult_of P) d a)) ?T"
    by (simp add:nat_pow_mult_of)
  also have "... = ?rhs"
    using fin_T a
    by (subst p.finprod_mult_of, simp_all add:pmult_def)
  finally have "?lhs ∼⇘(mult_of P)⇙ ?rhs" by simp
  moreover have "monic_poly R ?rhs"
    using fin_T
    by (intro monic_poly_prod monic_poly_pow)
      (auto simp:monic_irreducible_poly_def)
  ultimately show "?lhs = ?rhs"
    using monic_poly_not_assoc assms monic_irreducible_poly_def
    by blast
qed

lemma degree_monic_poly':
  assumes "monic_poly R f"
  shows
    "sum' (λd. pmult d f * degree d) {d. monic_irreducible_poly R d} =
    degree f"
proof -
  let ?mip = "monic_irreducible_poly R"

  have b: "d ∈ carrier P - {𝟬⇘P⇙}" if "?mip d" for d
    using that monic_poly_carr_2
    unfolding monic_irreducible_poly_def by simp
  have a: "d [^]⇘P⇙ n ∈ carrier P - {𝟬⇘P⇙}" if "?mip d" for d and n :: "nat"
    using b that monic_poly_pow
    unfolding monic_irreducible_poly_def
    by (simp add: p.pow_non_zero)

  have "degree f =
    degree (⨂⇘P⇙d∈{d. ?mip d ∧ pmult d f > 0}. d [^]⇘P⇙ pmult d f)"
    using factor_monic_poly[OF assms(1)] by simp
  also have "... =
    (∑i∈{d. ?mip d ∧ 0 < pmult d f}. degree (i [^]⇘P⇙ pmult i f))"
    using a assms(1)
    by (subst degree_prod[OF factor_monic_poly_fin])
     (simp_all add:Pi_def)
  also have "... =
    (∑i∈{d. ?mip d ∧ 0 < pmult d f}. degree i * pmult i f)"
    using b degree_pow by (intro sum.cong, auto)
  also have "... =
    (∑d∈{d. ?mip d ∧ 0 < pmult d f}. pmult d f * degree d)"
    by (simp add:mult.commute)
  also have "... =
    sum' (λd. pmult d f * degree d) {d. ?mip d ∧ 0 < pmult d f}"
    using sum.eq_sum factor_monic_poly_fin[OF assms(1)] by simp
  also have "... = sum' (λd. pmult d f * degree d) {d. ?mip d}"
    by (intro sum.mono_neutral_cong_left' subsetI, auto)
  finally show ?thesis by simp
qed

lemma monic_poly_min_degree:
  assumes "monic_irreducible_poly R f"
  shows  "degree f ≥ 1"
  using assms unfolding monic_irreducible_poly_def monic_poly_def
  by (intro pirreducible_degree) auto

lemma degree_one_monic_poly:
  "monic_irreducible_poly R f ∧ degree f = 1 ⟷
  (∃x ∈ carrier R. f = [𝟭, ⊖x])"
proof
  assume "monic_irreducible_poly R f ∧ degree f = 1"
  hence a:"monic_poly R f" "length f = 2"
    unfolding monic_irreducible_poly_def by auto
  then obtain u v where f_def: "f = [u,v]"
    by (cases f, simp, cases "tl f", auto)

  have "u = 𝟭" using a unfolding monic_poly_def f_def by simp
  moreover have "v ∈ carrier R"
    using a unfolding monic_poly_def univ_poly_carrier[symmetric]
    unfolding polynomial_def f_def by simp
  ultimately have "f =  [𝟭, ⊖(⊖v)]" "(⊖v) ∈ carrier R"
    using a_inv_closed f_def by auto
  thus "(∃x ∈ carrier R. f = [𝟭⇘R⇙, ⊖⇘R⇙x])" by auto
next
  assume "(∃x ∈ carrier R. f = [𝟭, ⊖x])"
  then obtain x where f_def: "f = [𝟭,⊖x]" "x ∈ carrier R" by auto
  have a:"degree f = 1" using f_def(2) unfolding f_def by simp
  have b:"f ∈ carrier P"
    using f_def(2) unfolding univ_poly_carrier[symmetric]
    unfolding f_def polynomial_def by simp
  have c: "pirreducible (carrier R) f"
    by (intro degree_one_imp_pirreducible a b)
  have d: "lead_coeff f = 𝟭" unfolding f_def by simp
  show "monic_irreducible_poly R f ∧ degree f = 1"
    using a b c d
    unfolding monic_irreducible_poly_def monic_poly_def
    by auto
qed

lemma multiplicity_ge_iff:
  assumes "monic_irreducible_poly R d"
  assumes "f ∈ carrier P - {𝟬⇘P⇙}"
  shows "pmult d f ≥ k ⟷ d [^]⇘P⇙ k pdivides f"
proof -
  have a:"f ∈ carrier (mult_of P)"
    using assms(2) by simp
  have b: "d ∈ carrier (mult_of P)"
    using assms(1) monic_poly_carr_2
    unfolding monic_irreducible_poly_def by simp
  have c: "irreducible (mult_of P) d"
    using assms(1) monic_poly_carr_2
    using p.irreducible_imp_irreducible_mult
    unfolding monic_irreducible_poly_def
    unfolding ring_irreducible_def monic_poly_def
    by simp
  have d: "d [^]⇘P⇙ k ∈ carrier P" using b by simp

  have "pmult d f ≥ k ⟷ d [^]⇘(mult_of P)⇙ k divides⇘(mult_of P)⇙ f"
    unfolding pmult_def
    by (intro p.mult_of.multiplicity_ge_iff a b c)
  also have "... ⟷ d [^]⇘P⇙ k pdivides⇘R⇙ f"
    using p.divides_imp_divides_mult[OF d assms(2)]
    using divides_mult_imp_divides
    unfolding pdivides_def nat_pow_mult_of
    by auto
  finally show ?thesis by simp
qed

lemma multiplicity_ge_1_iff_pdivides:
  assumes "monic_irreducible_poly R d" "f ∈ carrier P - {𝟬⇘P⇙}"
  shows "pmult d f ≥ 1 ⟷ d pdivides f"
proof -
  have "d ∈ carrier P"
    using assms(1) monic_poly_carr
    unfolding monic_irreducible_poly_def
    by simp
  thus ?thesis
    using multiplicity_ge_iff[OF assms, where k="1"]
    by simp
qed

lemma divides_monic_poly:
  assumes "monic_poly R f" "monic_poly R g"
  assumes "⋀d. monic_irreducible_poly R d
    ⟹ pmult d f ≤ pmult d g"
  shows "f pdivides g"
proof -
  have a:"f ∈ carrier (mult_of P)" "g ∈ carrier (mult_of P)"
    using monic_poly_carr_2 assms(1,2) by auto

  have "f divides⇘(mult_of P)⇙ g"
    using assms(3) unfolding pmult_def
    by (intro p.mult_of.divides_iff_mult_mono
        [OF a monic_polys_are_canonical_irreducibles]) simp
  thus ?thesis
    unfolding pdivides_def using divides_mult_imp_divides by simp
qed

end

lemma monic_poly_hom:
  assumes "monic_poly R f"
  assumes "h ∈ ring_iso R S" "domain R" "domain S"
  shows "monic_poly S (map h f)"
proof -
  have c: "h ∈ ring_hom R S"
    using assms(2) ring_iso_def by auto
  have e: "f ∈ carrier (poly_ring R)"
    using assms(1) unfolding monic_poly_def by simp

  have a:"f ≠ []"
    using assms(1) unfolding monic_poly_def by simp
  hence "map h f ≠ []" by simp
  moreover have "lead_coeff f = 𝟭⇘R⇙"
    using assms(1) unfolding monic_poly_def by simp
  hence "lead_coeff (map h f) = 𝟭⇘S⇙"
    using ring_hom_one[OF c] by (simp add: hd_map[OF a])
  ultimately show ?thesis
    using carrier_hom[OF e assms(2-4)]
    unfolding monic_poly_def by simp
qed

lemma monic_irreducible_poly_hom:
  assumes "monic_irreducible_poly R f"
  assumes "h ∈ ring_iso R S" "domain R" "domain S"
  shows "monic_irreducible_poly S (map h f)"
proof -
  have a:
    "pirreducible⇘R⇙ (carrier R) f"
    "f ∈ carrier (poly_ring R)"
    "monic_poly R f"
    using assms(1)
    unfolding monic_poly_def monic_irreducible_poly_def
    by auto

  have "pirreducible⇘S⇙ (carrier S) (map h f)"
    using a pirreducible_hom assms by auto
  moreover have "monic_poly S (map h f)"
    using a monic_poly_hom[OF _ assms(2,3,4)] by simp
  ultimately show ?thesis
    unfolding monic_irreducible_poly_def by simp
qed

end