Theory Algebraic_Numbers

(*  
    Author:       René Thiemann 
                  Akihisa Yamada
    Contributors: Manuel Eberl (algebraic integers)
    License:      BSD
*)
section ‹Algebraic Numbers: Addition and Multiplication›

text ‹This theory contains the remaining field operations for algebraic numbers, namely
  addition and multiplication.›

theory Algebraic_Numbers
  imports
  Algebraic_Numbers_Prelim
  Resultant
  Polynomial_Factorization.Polynomial_Irreducibility
begin

interpretation coeff_hom: monoid_add_hom "λp. coeff p i" by (unfold_locales, auto)
interpretation coeff_hom: comm_monoid_add_hom "λp. coeff p i"..
interpretation coeff_hom: group_add_hom "λp. coeff p i"..
interpretation coeff_hom: ab_group_add_hom "λp. coeff p i"..
interpretation coeff_0_hom: monoid_mult_hom "λp. coeff p 0" by (unfold_locales, auto simp: coeff_mult)
interpretation coeff_0_hom: semiring_hom "λp. coeff p 0"..
interpretation coeff_0_hom: comm_monoid_mult_hom "λp. coeff p 0"..
interpretation coeff_0_hom: comm_semiring_hom "λp. coeff p 0"..

subsection ‹Addition of Algebraic Numbers›

definition "x_y  [: [: 0, 1 :], -1 :]"

definition "poly_x_minus_y p = poly_lift p p x_y"

lemma coeff_xy_power:
  assumes "k  n"
  shows  "coeff (x_y ^ n :: 'a :: comm_ring_1 poly poly) k =
          monom (of_nat (n choose (n - k)) * (- 1) ^ k) (n - k)"
proof -
  define X :: "'a poly poly" where "X = monom (monom 1 1) 0"
  define Y :: "'a poly poly" where "Y = monom (-1) 1"

  have [simp]: "monom 1 b * (-1) ^ k = monom ((-1)^k :: 'a) b" for b k
    by (auto simp: monom_altdef minus_one_power_iff)

  have "(X + Y) ^ n = (in. of_nat (n choose i) * X ^ i * Y ^ (n - i))"
    by (subst binomial_ring) auto
  also have " = (in. of_nat (n choose i) * monom (monom ((-1) ^ (n - i)) i) (n - i))"
    by (simp add: X_def Y_def monom_power mult_monom mult.assoc) 
  also have " = (in. monom (monom (of_nat (n choose i) * (-1) ^ (n - i)) i) (n - i))"
    by (simp add: of_nat_poly smult_monom)
  also have "coeff  k =
    (in. if n - i = k then monom (of_nat (n choose i) * (- 1) ^ (n - i)) i else 0)"
    by (simp add: of_nat_poly coeff_sum)
  also have " = (i{n-k}. monom (of_nat (n choose i) * (- 1) ^ (n - i)) i)"
    using k  n by (intro sum.mono_neutral_cong_right) auto
  also have "X + Y = x_y"
    by (simp add: X_def Y_def x_y_def monom_altdef)
  finally show ?thesis
    using k  n by simp
qed


text ‹The following polynomial represents the sum of two algebraic numbers.›

definition poly_add :: "'a :: comm_ring_1 poly  'a poly  'a poly" where
  "poly_add p q = resultant (poly_x_minus_y p) (poly_lift q)"

subsubsection @{term poly_add} has desired root›

interpretation poly_x_minus_y_hom:
  comm_ring_hom poly_x_minus_y by (unfold_locales; simp add: poly_x_minus_y_def hom_distribs)

lemma poly2_x_y[simp]:
  fixes x :: "'a :: comm_ring_1"
  shows "poly2 x_y x y = x - y" unfolding poly2_def by (simp add: x_y_def)

lemma degree_poly_x_minus_y[simp]:
  fixes p :: "'a::idom poly"
  shows "degree (poly_x_minus_y p) = degree p" unfolding poly_x_minus_y_def x_y_def by auto

lemma poly_x_minus_y_pCons[simp]:
  "poly_x_minus_y (pCons a p) = [:[: a :]:] + poly_x_minus_y p * x_y"
  unfolding poly_x_minus_y_def x_y_def by simp

lemma poly_poly_poly_x_minus_y[simp]:
  fixes p :: "'a :: comm_ring_1 poly"
  shows "poly (poly (poly_x_minus_y p) q) x = poly p (x - poly q x)"
  by (induct p; simp add: ring_distribs x_y_def)

lemma poly2_poly_x_minus_y[simp]:
  fixes p :: "'a :: comm_ring_1 poly"
  shows "poly2 (poly_x_minus_y p) x y = poly p (x-y)" unfolding poly2_def by simp

interpretation x_y_mult_hom: zero_hom_0 "λp :: 'a :: comm_ring_1 poly poly. x_y * p"
proof (unfold_locales)
  fix p :: "'a poly poly"
  assume "x_y * p = 0"
  then show "p = 0" apply (simp add: x_y_def)
    by (metis eq_neg_iff_add_eq_0 minus_equation_iff minus_pCons synthetic_div_unique_lemma)
qed

lemma x_y_nonzero[simp]: "x_y  0" by (simp add: x_y_def)

lemma degree_x_y[simp]: "degree x_y = 1" by (simp add: x_y_def)

interpretation x_y_mult_hom: inj_comm_monoid_add_hom "λp :: 'a :: idom poly poly. x_y * p"
proof (unfold_locales)
  show "x_y * p = x_y * q  p = q" for p q :: "'a poly poly"
  proof (induct p arbitrary:q)
    case 0
    then show ?case by simp
  next
    case p: (pCons a p)
    from p(3)[unfolded mult_pCons_right]
    have "x_y * (monom a 0 + pCons 0 1 * p) = x_y * q"
      apply (subst(asm) pCons_0_as_mult)
      apply (subst(asm) smult_prod) by (simp only: field_simps distrib_left)
    then have "monom a 0 + pCons 0 1 * p = q" by simp
    then show "pCons a p = q" using pCons_as_add by (simp add: monom_0 monom_Suc)
  qed
qed

interpretation poly_x_minus_y_hom: inj_idom_hom poly_x_minus_y
proof
  fix p :: "'a poly"
  assume 0: "poly_x_minus_y p = 0"
  then have "poly_lift p p x_y = 0" by (simp add: poly_x_minus_y_def)
  then show "p = 0"
  proof (induct p)
    case 0
    then show ?case by simp
  next
    case (pCons a p)
    note p = this[unfolded poly_lift_pCons pcompose_pCons]
    show ?case
    proof (cases "a=0")
      case a0: True
      with p have "x_y * poly_lift p p x_y = 0" by simp
      then have "poly_lift p p x_y = 0" by simp
      then show ?thesis using p by simp
    next
      case a0: False
      with p have p0: "p  0" by auto
      from p have "[:[:a:]:] = - x_y * poly_lift p p x_y" by (simp add: eq_neg_iff_add_eq_0)
      then have "degree [:[:a:]:] = degree (x_y * poly_lift p p x_y)" by simp
      also have "... = degree (x_y::'a poly poly) + degree (poly_lift p p x_y)"
        apply (subst degree_mult_eq)
          apply simp
         apply (subst pcompose_eq_0)
          apply (simp add: x_y_def)
         apply (simp add: p0)
        apply simp
       done
      finally have False by simp 
      then show ?thesis..
    qed
  qed
qed

lemma poly_add:
  fixes p q :: "'a ::comm_ring_1 poly"
  assumes q0: "q  0" and x: "poly p x = 0" and y: "poly q y = 0"
  shows "poly (poly_add p q) (x+y) = 0"
proof (unfold poly_add_def, rule poly_resultant_zero[OF disjI2])
  have "degree q > 0" using poly_zero q0 y by auto
  thus degq: "degree (poly_lift q) > 0" by auto
qed (insert x y, simp_all)


subsubsection @{const poly_add} is nonzero›

text ‹
  We first prove that @{const poly_lift} preserves factorization. The result will be essential
  also in the next section for division of algebraic numbers.
›

interpretation poly_lift_hom:
  unit_preserving_hom "poly_lift :: 'a :: {comm_semiring_1,semiring_no_zero_divisors} poly  _"
proof
  fix x :: "'a poly"
  assume "poly_lift x dvd 1"
  then have "poly_y_x (poly_lift x) dvd poly_y_x 1"
    by simp
  then show "x dvd 1"
    by (auto simp add: poly_y_x_poly_lift)
qed

interpretation poly_lift_hom:
  factor_preserving_hom "poly_lift::'a::idom poly  'a poly poly"
proof unfold_locales
  fix p :: "'a poly"
  assume p: "irreducible p"
  show "irreducible (poly_lift p)"
  proof(rule ccontr)
    from p have p0: "p  0" and "¬ p dvd 1" by (auto dest: irreducible_not_unit)
    with poly_lift_hom.hom_dvd[of p 1] have p1: "¬ poly_lift p dvd 1" by auto
    assume "¬ irreducible (poly_lift p)"
    from this[unfolded irreducible_altdef,simplified] p0 p1
    obtain q where "q dvd poly_lift p" and pq: "¬ poly_lift p dvd q" and q: "¬ q dvd 1" by auto
    then obtain r where "q * r = poly_lift p" by (elim dvdE, auto)
    then have "poly_y_x (q * r) = poly_y_x (poly_lift p)" by auto
    also have "... = [:p:]" by (auto simp: poly_y_x_poly_lift monom_0)
    also have "poly_y_x (q * r) = poly_y_x q * poly_y_x r" by (auto simp: hom_distribs)
    finally have "... = [:p:]" by auto
    then have qp: "poly_y_x q dvd [:p:]" by (metis dvdI)
    from dvd_const[OF this] p0 have "degree (poly_y_x q) = 0" by auto
    from degree_0_id[OF this,symmetric] obtain s
      where qs: "poly_y_x q = [:s:]" by auto
    have "poly_lift s = poly_y_x (poly_y_x (poly_lift s))" by auto
      also have "... = poly_y_x [:s:]" by (auto simp: poly_y_x_poly_lift monom_0)
      also have "... = q" by (auto simp: qs[symmetric])
    finally have sq: "poly_lift s = q" by auto
    from qp[unfolded qs] have sp: "s dvd p" by (auto simp: const_poly_dvd)
    from irreducibleD'[OF p this] sq q pq show False by auto
  qed
qed

text ‹
  We now show that @{const poly_x_minus_y} is a factor-preserving homomorphism. This is
  essential for this section. This is easy since @{const poly_x_minus_y} can be represented
  as the composition of two factor-preserving homomorphisms.
›

lemma poly_x_minus_y_as_comp: "poly_x_minus_y = (λp. p p x_y)  poly_lift"
  by (intro ext, unfold poly_x_minus_y_def, auto)
context idom_isom begin
  sublocale comm_semiring_isom..
end

interpretation poly_x_minus_y_hom:
  factor_preserving_hom "poly_x_minus_y :: 'a :: idom poly  'a poly poly"
proof -
  have p p x_y p x_y = p for p :: 'a poly poly
  proof (induction p)
    case 0
    show ?case
      by simp
  next
    case (pCons a p)
    then show ?case
      by (unfold x_y_def hom_distribs pcompose_pCons) simp
  qed
  then interpret x_y_hom: bijective "λp :: 'a poly poly. p p x_y"
    by (unfold bijective_eq_bij) (rule involuntory_imp_bij)
  interpret x_y_hom: idom_isom "λp :: 'a poly poly. p p x_y"
    by standard simp_all
  have factor_preserving_hom (λp :: 'a poly poly. p p x_y)
    and factor_preserving_hom (poly_lift :: 'a poly  'a poly poly)
    ..
  then show "factor_preserving_hom (poly_x_minus_y :: 'a poly  _)"
    by (unfold poly_x_minus_y_as_comp) (rule factor_preserving_hom_comp)
qed

text ‹
  Now we show that results of @{const poly_x_minus_y} and @{const poly_lift} are coprime.
›

lemma poly_y_x_const[simp]: "poly_y_x [:[:a:]:] = [:[:a:]:]" by (simp add: poly_y_x_def monom_0)

context begin

private abbreviation "y_x == [: [: 0, -1 :], 1 :]"

lemma poly_y_x_x_y[simp]: "poly_y_x x_y = y_x" by (simp add: x_y_def poly_y_x_def monom_Suc monom_0)

private lemma y_x[simp]: fixes x :: "'a :: comm_ring_1" shows "poly2 y_x x y = y - x"
  unfolding poly2_def by simp

private definition "poly_y_minus_x p  poly_lift p p y_x"

private lemma poly_y_minus_x_0[simp]: "poly_y_minus_x 0 = 0" by (simp add: poly_y_minus_x_def)

private lemma poly_y_minus_x_pCons[simp]:
  "poly_y_minus_x (pCons a p) = [:[: a :]:] + poly_y_minus_x p * y_x" by (simp add: poly_y_minus_x_def)

private lemma poly_y_x_poly_x_minus_y:
  fixes p :: "'a :: idom poly"
  shows "poly_y_x (poly_x_minus_y p) = poly_y_minus_x p"
  apply (induct p, simp)
  apply (unfold poly_x_minus_y_pCons hom_distribs) by simp

lemma degree_poly_y_minus_x[simp]:
  fixes p :: "'a :: idom poly"
  shows "degree (poly_y_x (poly_x_minus_y p)) = degree p" 
  by (simp add: poly_y_minus_x_def poly_y_x_poly_x_minus_y)

end

lemma dvd_all_coeffs_iff:
  fixes x :: "'a :: comm_semiring_1" (* No addition needed! *)
  shows "(pi  set (coeffs p). x dvd pi)  (i. x dvd coeff p i)" (is "?l = ?r")
proof-
  have "?r = (i{..degree p}  {Suc (degree p)..}. x dvd coeff p i)" by auto
  also have "... = (idegree p. x dvd coeff p i)" by (auto simp add: ball_Un coeff_eq_0)
  also have "... = ?l" by (auto simp: coeffs_def)
  finally show ?thesis..
qed

lemma primitive_imp_no_constant_factor:
  fixes p :: "'a :: {comm_semiring_1, semiring_no_zero_divisors} poly"
  assumes pr: "primitive p" and F: "mset_factors F p" and fF: "f ∈# F"
  shows "degree f  0"
proof
  from F fF have irr: "irreducible f" and fp: "f dvd p" by (auto dest: mset_factors_imp_dvd)
  assume deg: "degree f = 0"
  then obtain f0 where f0: "f = [:f0:]" by (auto dest: degree0_coeffs)
  with fp have "[:f0:] dvd p" by simp
  then have "f0 dvd coeff p i" for i by (simp add: const_poly_dvd_iff)
  with primitiveD[OF pr] dvd_all_coeffs_iff have "f0 dvd 1" by (auto simp: coeffs_def)
  with f0 irr show False by auto
qed

lemma coprime_poly_x_minus_y_poly_lift:
  fixes p q :: "'a :: ufd poly"
  assumes degp: "degree p > 0" and degq: "degree q > 0"
    and pr: "primitive p"
  shows "coprime (poly_x_minus_y p) (poly_lift q)"
proof(rule ccontr)
  from degp have p: "¬ p dvd 1" by (auto simp: dvd_const)
  from degp have p0: "p  0" by auto
  from mset_factors_exist[of p, OF p0 p]
  obtain F where F: "mset_factors F p" by auto
  with poly_x_minus_y_hom.hom_mset_factors
  have pF: "mset_factors (image_mset poly_x_minus_y F) (poly_x_minus_y p)" by auto

  from degq have q: "¬ q dvd 1" by (auto simp: dvd_const)
  from degq have q0: "q  0" by auto
  from mset_factors_exist[OF q0 q]
  obtain G where G: "mset_factors G q" by auto
  with poly_lift_hom.hom_mset_factors
  have pG: "mset_factors (image_mset poly_lift G) (poly_lift q)" by auto

  assume "¬ coprime (poly_x_minus_y p) (poly_lift q)"
  from this[unfolded not_coprime_iff_common_factor]
  obtain r
  where rp: "r dvd (poly_x_minus_y p)"
    and rq: "r dvd (poly_lift q)"
    and rU: "¬ r dvd 1" by auto note poly_lift_hom.hom_dvd
  from rp p0 have r0: "r  0" by auto
  from mset_factors_exist[OF r0 rU]
  obtain H where H: "mset_factors H r" by auto
  then have "H  {#}" by auto
  then obtain h where hH: "h ∈# H" by fastforce
  with H mset_factors_imp_dvd have hr: "h dvd r" and h: "irreducible h" by auto
  from irreducible_not_unit[OF h] have hU: "¬ h dvd 1" by auto
  from hr rp have "h dvd (poly_x_minus_y p)" by (rule dvd_trans)
  from irreducible_dvd_imp_factor[OF this h pF] p0
  obtain f where f: "f ∈# F" and fh: "poly_x_minus_y f ddvd h" by auto
  from hr rq have "h dvd (poly_lift q)" by (rule dvd_trans)
  from irreducible_dvd_imp_factor[OF this h pG] q0
  obtain g where g: "g ∈# G" and gh: "poly_lift g ddvd h" by auto
  from fh gh have "poly_x_minus_y f ddvd poly_lift g" using ddvd_trans by auto
  then have "poly_y_x (poly_x_minus_y f) ddvd poly_y_x (poly_lift g)" by simp
  also have "poly_y_x (poly_lift g) = [:g:]" unfolding poly_y_x_poly_lift monom_0 by auto
  finally have ddvd: "poly_y_x (poly_x_minus_y f) ddvd [:g:]" by auto
  then have "degree (poly_y_x (poly_x_minus_y f)) = 0" by (metis degree_pCons_0 dvd_0_left_iff dvd_const)
  then have "degree f = 0" by simp
  with primitive_imp_no_constant_factor[OF pr F f] show False by auto
qed

lemma poly_add_nonzero:
  fixes p q :: "'a :: ufd poly"
  assumes p0: "p  0" and q0: "q  0" and x: "poly p x = 0" and y: "poly q y = 0"
      and pr: "primitive p"
  shows "poly_add p q  0"
proof
  have degp: "degree p > 0" using le_0_eq order_degree order_root p0 x by (metis gr0I)
  have degq: "degree q > 0" using le_0_eq order_degree order_root q0 y by (metis gr0I)
  assume 0: "poly_add p q = 0"
  from resultant_zero_imp_common_factor[OF _ this[unfolded poly_add_def]] degp
   and coprime_poly_x_minus_y_poly_lift[OF degp degq pr]
  show False by auto
qed


subsubsection ‹Summary for addition›

text ‹Now we lift the results to one that uses @{const ipoly}, by showing some homomorphism lemmas.›

lemma (in comm_ring_hom) map_poly_x_minus_y:
  "map_poly (map_poly hom) (poly_x_minus_y p) = poly_x_minus_y (map_poly hom p)"
proof-
  interpret mp: map_poly_comm_ring_hom hom..
  interpret mmp: map_poly_comm_ring_hom "map_poly hom"..
  show ?thesis
    apply (induct p, simp)
    apply(unfold x_y_def hom_distribs poly_x_minus_y_pCons, simp) done
qed

lemma (in comm_ring_hom) hom_poly_lift[simp]:
  "map_poly (map_poly hom) (poly_lift q) = poly_lift (map_poly hom q)"
proof -
  show ?thesis
    unfolding poly_lift_def
    unfolding map_poly_map_poly[of coeff_lift,OF coeff_lift_hom.hom_zero]
    unfolding map_poly_coeff_lift_hom by simp
qed


lemma lead_coeff_poly_x_minus_y:
  fixes p :: "'a::idom poly"
  shows "lead_coeff (poly_x_minus_y p) = [:lead_coeff p * ((- 1) ^ degree p):]" (is "?l = ?r")
proof-
  have "?l = Polynomial.smult (lead_coeff p) ((- 1) ^ degree p)"
    by (unfold poly_x_minus_y_def, subst lead_coeff_comp; simp add: x_y_def)
  also have "... = ?r" by (unfold hom_distribs, simp add: smult_as_map_poly[symmetric])
  finally show ?thesis.
qed

lemma degree_coeff_poly_x_minus_y:
  fixes p q :: "'a :: {idom, semiring_char_0} poly"
  shows "degree (coeff (poly_x_minus_y p) i) = degree p - i"
proof -
  consider "i = degree p" | "i > degree p" | "i < degree p"
    by force
  thus ?thesis
  proof cases
    assume "i > degree p"
    thus ?thesis by (subst coeff_eq_0) auto
  next
    assume "i = degree p"
    thus ?thesis using lead_coeff_poly_x_minus_y[of p]
      by (simp add: lead_coeff_poly_x_minus_y)
  next
    assume "i < degree p"
    define n where "n = degree p"
    have "degree (coeff (poly_x_minus_y p) i) =
            degree (jn. [:coeff p j:] * coeff (x_y ^ j) i)" (is "_ = degree (sum ?f _)")
      by (simp add: poly_x_minus_y_def pcompose_conv_poly poly_altdef coeff_sum n_def)
    also have "{..n} = insert n {..<n}"
      by auto
    also have "sum ?f  = ?f n + sum ?f {..<n}"
      by (subst sum.insert) auto
    also have "degree  = n - i"
    proof -
      have "degree (?f n) = n - i"
        using i < degree p by (simp add: n_def coeff_xy_power degree_monom_eq)
      moreover have "degree (sum ?f {..<n}) < n - i"
      proof (intro degree_sum_smaller)
        fix j assume "j  {..<n}"
        have "degree ([:coeff p j:] * coeff (x_y ^ j) i)  j - i"
        proof (cases "i  j")
          case True
          thus ?thesis
            by (auto simp: n_def coeff_xy_power degree_monom_eq)
        next
          case False
          hence "coeff (x_y ^ j :: 'a poly poly) i = 0"
            by (subst coeff_eq_0) (auto simp: degree_power_eq)
          thus ?thesis by simp
        qed
        also have " < n - i"
          using j  {..<n} i < degree p by (auto simp: n_def)
        finally show "degree ([:coeff p j:] * coeff (x_y ^ j) i) < n - i" .
      qed (use i < degree p in auto simp: n_def)
      ultimately show ?thesis
        by (subst degree_add_eq_left) auto
    qed
    finally show ?thesis
      by (simp add: n_def)
  qed
qed

lemma coeff_0_poly_x_minus_y [simp]: "coeff (poly_x_minus_y p) 0 = p"
  by (induction p) (auto simp: poly_x_minus_y_def x_y_def)

lemma (in idom_hom) poly_add_hom:
  assumes p0: "hom (lead_coeff p)  0" and q0: "hom (lead_coeff q)  0"
  shows "map_poly hom (poly_add p q) = poly_add (map_poly hom p) (map_poly hom q)"
proof -
  interpret mh: map_poly_idom_hom..
  show ?thesis unfolding poly_add_def
    apply (subst mh.resultant_map_poly(1)[symmetric])
       apply (subst degree_map_poly_2)
       apply (unfold lead_coeff_poly_x_minus_y, unfold hom_distribs, simp add: p0)
      apply simp
     apply (subst degree_map_poly_2)
      apply (simp_all add: q0 map_poly_x_minus_y)
    done
qed

lemma(in zero_hom) hom_lead_coeff_nonzero_imp_map_poly_hom:
  assumes "hom (lead_coeff p)  0"
  shows "map_poly hom p  0"
proof
  assume "map_poly hom p = 0"
  then have "coeff (map_poly hom p) (degree p) = 0" by simp
  with assms show False by simp
qed

lemma ipoly_poly_add:
  fixes x y :: "'a :: idom"
  assumes p0: "(of_int (lead_coeff p) :: 'a)  0" and q0: "(of_int (lead_coeff q) :: 'a)  0"
      and x: "ipoly p x = 0" and y: "ipoly q y = 0"
  shows "ipoly (poly_add p q) (x+y) = 0"
  using assms of_int_hom.hom_lead_coeff_nonzero_imp_map_poly_hom[OF q0]
  by (auto intro: poly_add simp: of_int_hom.poly_add_hom[OF p0 q0])

lemma (in comm_monoid_gcd) gcd_list_eq_0_iff[simp]: "listgcd xs = 0  (x  set xs. x = 0)"
  by (induct xs, auto)

lemma primitive_field_poly[simp]: "primitive (p :: 'a :: field poly)  p  0"
  by (unfold primitive_iff_some_content_dvd_1,auto simp: dvd_field_iff coeffs_def)

lemma ipoly_poly_add_nonzero:
  fixes x y :: "'a :: field"
  assumes "p  0" and "q  0" and "ipoly p x = 0" and "ipoly q y = 0"
      and "(of_int (lead_coeff p) :: 'a)  0" and "(of_int (lead_coeff q) :: 'a)  0"
  shows "poly_add p q  0"
proof-
  from assms have "(of_int_poly (poly_add p q) :: 'a poly)  0"
    apply (subst of_int_hom.poly_add_hom,simp,simp)
    by (rule poly_add_nonzero, auto dest:of_int_hom.hom_lead_coeff_nonzero_imp_map_poly_hom)
  then show ?thesis by auto
qed

lemma represents_add:
  assumes x: "p represents x" and y: "q represents y"
  shows "(poly_add p q) represents (x + y)"
  using assms by (intro representsI ipoly_poly_add ipoly_poly_add_nonzero, auto)

subsection ‹Division of Algebraic Numbers›

definition poly_x_mult_y where
  [code del]: "poly_x_mult_y p  ( i  degree p. monom (monom (coeff p i) i) i)"

lemma coeff_poly_x_mult_y:
  shows "coeff (poly_x_mult_y p) i = monom (coeff p i) i" (is "?l = ?r")
proof(cases "degree p < i")
  case i: False
  have "?l = sum (λj. if j = i then (monom (coeff p j) j) else 0) {..degree p}"
   (is "_ = sum ?f ?A") by (simp add: poly_x_mult_y_def coeff_sum)
  also have "... = sum ?f {i}" using i by (intro sum.mono_neutral_right, auto)
  also have "... = ?f i" by simp
  also have "... = ?r" by auto
  finally show ?thesis.
next
  case True then show ?thesis by (auto simp: poly_x_mult_y_def coeff_eq_0 coeff_sum)
qed

lemma poly_x_mult_y_code[code]: "poly_x_mult_y p = (let cs = coeffs p
  in poly_of_list (map (λ (i, ai). monom ai i) (zip [0 ..< length cs] cs)))" 
  unfolding Let_def poly_of_list_def 
proof (rule poly_eqI, unfold coeff_poly_x_mult_y)
  fix n
  let ?xs = "zip [0..<length (coeffs p)] (coeffs p)" 
  let ?f = "(λ(i, ai). monom ai i)" 
  show "monom (coeff p n) n = coeff (Poly (map ?f ?xs)) n" 
  proof (cases "n < length (coeffs p)")
    case True
    hence n: "n < length (map ?f ?xs)" and nn: "n < length ?xs" 
      unfolding degree_eq_length_coeffs by auto
    show ?thesis unfolding coeff_Poly nth_default_nth[OF n] nth_map[OF nn]
      using True by (simp add: nth_coeffs_coeff)
  next
    case False
    hence id: "coeff (Poly (map ?f ?xs)) n = 0" unfolding coeff_Poly
      by (subst nth_default_beyond, auto)
    from False have "n > degree p  p = 0" unfolding degree_eq_length_coeffs by (cases n, auto)
    hence "monom (coeff p n) n = 0" using coeff_eq_0[of p n] by auto
    thus ?thesis unfolding id by simp
  qed
qed

definition poly_div :: "'a :: comm_ring_1 poly  'a poly  'a poly" where
  "poly_div p q = resultant (poly_x_mult_y p) (poly_lift q)"

text @{const poly_div} has desired roots.›

lemma poly2_poly_x_mult_y:
  fixes p :: "'a :: comm_ring_1 poly"
  shows "poly2 (poly_x_mult_y p) x y = poly p (x * y)"
  apply (subst(3) poly_as_sum_of_monoms[symmetric])
  apply (unfold poly_x_mult_y_def hom_distribs)
  by (auto simp: poly2_monom poly_monom power_mult_distrib ac_simps)

lemma poly_div:
  fixes p q :: "'a ::field poly"
  assumes q0: "q  0" and x: "poly p x = 0" and y: "poly q y = 0" and y0: "y  0"
  shows "poly (poly_div p q) (x/y) = 0"
proof (unfold poly_div_def, rule poly_resultant_zero[OF disjI2])
  have "degree q > 0" using poly_zero q0 y by auto
  thus degq: "degree (poly_lift q) > 0" by auto
qed (insert x y y0, simp_all add: poly2_poly_x_mult_y)


text @{const poly_div} is nonzero.›

interpretation poly_x_mult_y_hom: ring_hom "poly_x_mult_y :: 'a :: {idom,ring_char_0} poly  _"
  by (unfold_locales, auto intro: poly2_ext simp: poly2_poly_x_mult_y hom_distribs)

interpretation poly_x_mult_y_hom: inj_ring_hom "poly_x_mult_y :: 'a :: {idom,ring_char_0} poly  _"
proof
  let ?h = poly_x_mult_y
  fix f :: "'a poly"
  assume "?h f = 0"
  then have "poly2 (?h f) x 1 = 0" for x by simp
  from this[unfolded poly2_poly_x_mult_y]
  show "f = 0" by auto
qed

lemma degree_poly_x_mult_y[simp]:
  fixes p :: "'a :: {idom, ring_char_0} poly"
  shows "degree (poly_x_mult_y p) = degree p" (is "?l = ?r")
proof(rule antisym)
  show "?r  ?l" by (cases "p=0", auto intro: le_degree simp: coeff_poly_x_mult_y)
  show "?l  ?r" unfolding poly_x_mult_y_def
    by (auto intro: degree_sum_le le_trans[OF degree_monom_le])
qed

interpretation poly_x_mult_y_hom: unit_preserving_hom "poly_x_mult_y :: 'a :: field_char_0 poly  _"
proof(unfold_locales)
  let ?h = "poly_x_mult_y :: 'a poly  _"
  fix f :: "'a poly"
  assume unit: "?h f dvd 1"
  then have "degree (?h f) = 0" and "coeff (?h f) 0 dvd 1" unfolding poly_dvd_1 by auto
  then have deg: "degree f = 0" by (auto simp add: degree_monom_eq)
  with unit show "f dvd 1" by(cases "f = 0", auto)
qed

lemmas poly_y_x_o_poly_lift = o_def[of poly_y_x poly_lift, unfolded poly_y_x_poly_lift]

lemma irreducible_dvd_degree: assumes "(f::'a::field poly) dvd g"
 "irreducible g"
 "degree f > 0"
 shows "degree f = degree g"
  using assms
 by (metis irreducible_altdef degree_0 dvd_refl is_unit_field_poly linorder_neqE_nat poly_divides_conv0)

lemma coprime_poly_x_mult_y_poly_lift:
  fixes p q :: "'a :: field_char_0 poly"
  assumes degp: "degree p > 0" and degq: "degree q > 0"
    and nz: "poly p 0  0  poly q 0  0" 
  shows "coprime (poly_x_mult_y p) (poly_lift q)"
proof(rule ccontr)
  from degp have p: "¬ p dvd 1" by (auto simp: dvd_const)
  from degp have p0: "p  0" by auto
  from mset_factors_exist[of p, OF p0 p]
  obtain F where F: "mset_factors F p" by auto
  then have pF: "prod_mset (image_mset poly_x_mult_y F) = poly_x_mult_y p"
    by (auto simp: hom_distribs)

  from degq have q: "¬ is_unit q" by (auto simp: dvd_const)
  from degq have q0: "q  0" by auto
  from mset_factors_exist[OF q0 q]
  obtain G where G: "mset_factors G q" by auto
  with poly_lift_hom.hom_mset_factors
  have pG: "mset_factors (image_mset poly_lift G) (poly_lift q)" by auto
  from poly_y_x_hom.hom_mset_factors[OF this]
  have pG: "mset_factors (image_mset coeff_lift G) [:q:]"
    by (auto simp: poly_y_x_poly_lift monom_0 image_mset.compositionality poly_y_x_o_poly_lift)

  assume "¬ coprime (poly_x_mult_y p) (poly_lift q)"
  then have "¬ coprime (poly_y_x (poly_x_mult_y p)) (poly_y_x (poly_lift q))"
    by (simp del: coprime_iff_coprime)
  from this[unfolded not_coprime_iff_common_factor]
  obtain r
  where rp: "r dvd poly_y_x (poly_x_mult_y p)"
    and rq: "r dvd poly_y_x (poly_lift q)"
    and rU: "¬ r dvd 1" by auto
  from rp p0 have r0: "r  0" by auto
  from mset_factors_exist[OF r0 rU]
  obtain H where H: "mset_factors H r" by auto
  then have "H  {#}" by auto
  then obtain h where hH: "h ∈# H" by fastforce
  with H mset_factors_imp_dvd have hr: "h dvd r" and h: "irreducible h" by auto
  from irreducible_not_unit[OF h] have hU: "¬ h dvd 1" by auto
  from hr rp have "h dvd poly_y_x (poly_x_mult_y p)" by (rule dvd_trans)
  note this[folded pF,unfolded poly_y_x_hom.hom_prod_mset image_mset.compositionality]
  from prime_elem_dvd_prod_mset[OF h[folded prime_elem_iff_irreducible] this]
  obtain f where f: "f ∈# F" and hf: "h dvd poly_y_x (poly_x_mult_y f)" by auto
  have irrF: "irreducible f" using f F by blast
    from dvd_trans[OF hr rq] have "h dvd [:q:]" by (simp add: poly_y_x_poly_lift monom_0)
    from irreducible_dvd_imp_factor[OF this h pG] q0
    obtain g where g: "g ∈# G" and gh: "[:g:] dvd h" by auto
    from dvd_trans[OF gh hf] have *: "[:g:] dvd poly_y_x (poly_x_mult_y f)" using dvd_trans by auto
  show False
  proof (cases "poly f 0 = 0")
    case f_0: False
    from poly_hom.hom_dvd[OF *]
    have "g dvd poly (poly_y_x (poly_x_mult_y f)) [:0:]" by simp
    also have "... = [:poly f 0:]" by (intro poly_ext, fold poly2_def, simp add: poly2_poly_x_mult_y)
    also have "... dvd 1" using f_0 by auto
    finally have "g dvd 1".
    with g G show False by (auto elim!: mset_factorsE dest!: irreducible_not_unit)
  next
    case True
    hence "[:0,1:] dvd f" by (unfold dvd_iff_poly_eq_0, simp)
    from irreducible_dvd_degree[OF this irrF]
    have "degree f = 1" by auto
    from degree1_coeffs[OF this] True obtain c where c: "c  0" and f: "f = [:0,c:]" by auto
    from g G have irrG: "irreducible g" by auto
    from poly_hom.hom_dvd[OF *]
    have "g dvd poly (poly_y_x (poly_x_mult_y f)) 1" by simp
    also have " = f" by (auto simp: f poly_x_mult_y_code Let_def c poly_y_x_pCons map_poly_monom poly_monom poly_lift_def)
    also have " dvd [:0,1:]" unfolding f dvd_def using c 
      by (intro exI[of _ "[: inverse c :]"], auto)
    finally have g01: "g dvd [:0,1:]" .
    from divides_degree[OF this] irrG have "degree g = 1" by auto
    from degree1_coeffs[OF this] obtain a b where g: "g = [:b,a:]" and a: "a  0" by auto
    from g01[unfolded dvd_def] g obtain k where id: "[:0,1:] = g * k" by auto
    from id have 0: "g  0" "k  0" by auto
    from arg_cong[OF id, of degree] have "degree k = 0" unfolding degree_mult_eq[OF 0] 
      unfolding g using a by auto
    from degree0_coeffs[OF this] obtain kk where k: "k = [:kk:]" by auto
    from id[unfolded g k] a have "b = 0" by auto
    hence "poly g 0 = 0" by (auto simp: g)
    from True this nz f ∈# F g ∈# G F G
    show False by (auto dest!:mset_factors_imp_dvd elim:dvdE)
  qed
qed

lemma poly_div_nonzero:
  fixes p q :: "'a :: field_char_0 poly"
  assumes p0: "p  0" and q0: "q  0" and x: "poly p x = 0" and y: "poly q y = 0"
      and p_0: "poly p 0  0  poly q 0  0"
  shows "poly_div p q  0"
proof
  have degp: "degree p > 0" using le_0_eq order_degree order_root p0 x by (metis gr0I)
  have degq: "degree q > 0" using le_0_eq order_degree order_root q0 y by (metis gr0I)
  assume 0: "poly_div p q = 0"
  from resultant_zero_imp_common_factor[OF _ this[unfolded poly_div_def]] degp
   and coprime_poly_x_mult_y_poly_lift[OF degp degq] p_0
  show False by auto
qed

subsubsection ‹Summary for division›

text ‹Now we lift the results to one that uses @{const ipoly}, by showing some homomorphism lemmas.›

lemma (in inj_comm_ring_hom) poly_x_mult_y_hom:
  "poly_x_mult_y (map_poly hom p) = map_poly (map_poly hom) (poly_x_mult_y p)"
proof -
  interpret mh: map_poly_inj_comm_ring_hom..
  interpret mmh: map_poly_inj_comm_ring_hom "map_poly hom"..
  show ?thesis unfolding poly_x_mult_y_def by (simp add: hom_distribs)
qed

lemma (in inj_comm_ring_hom) poly_div_hom:
  "map_poly hom (poly_div p q) = poly_div (map_poly hom p) (map_poly hom q)"
proof -
  have zero: "x. hom x = 0  x = 0" by simp
  interpret mh: map_poly_inj_comm_ring_hom..
  show ?thesis unfolding poly_div_def mh.resultant_hom[symmetric]
    by (simp add: poly_x_mult_y_hom)
qed

lemma ipoly_poly_div:
  fixes x y :: "'a :: field_char_0"
  assumes "q  0" and "ipoly p x = 0" and "ipoly q y = 0" and "y  0"
  shows "ipoly (poly_div p q) (x/y) = 0"
  by (unfold of_int_hom.poly_div_hom, rule poly_div, insert assms, auto)

lemma ipoly_poly_div_nonzero:
  fixes x y :: "'a :: field_char_0"
  assumes "p  0" and "q  0" and "ipoly p x = 0" and "ipoly q y = 0" and "poly p 0  0  poly q 0  0"
  shows "poly_div p q  0"
proof-
  from assms have "(of_int_poly (poly_div p q) :: 'a poly)  0" using of_int_hom.poly_map_poly[of p]
    by (subst of_int_hom.poly_div_hom, subst poly_div_nonzero, auto) 
  then show ?thesis by auto
qed

lemma represents_div:
  fixes x y :: "'a :: field_char_0"
  assumes "p represents x" and "q represents y" and "poly q 0  0"
  shows "(poly_div p q) represents (x / y)"
  using assms by (intro representsI ipoly_poly_div ipoly_poly_div_nonzero, auto)


subsection ‹Multiplication of Algebraic Numbers›

definition poly_mult where "poly_mult p q  poly_div p (reflect_poly q)"

lemma represents_mult:
  assumes px: "p represents x" and qy: "q represents y" and q_0: "poly q 0  0" 
  shows "(poly_mult p q) represents (x * y)"
proof-
  from q_0 qy have y0: "y  0" by auto
  from represents_inverse[OF y0 qy] y0 px q_0
  have "poly_mult p q represents x / (inverse y)"
    unfolding poly_mult_def by (intro represents_div, auto)
  with y0 show ?thesis by (simp add: field_simps)
qed

subsection ‹Summary: Closure Properties of Algebraic Numbers›

lemma algebraic_representsI: "p represents x  algebraic x"
  unfolding represents_def algebraic_altdef_ipoly by auto

lemma algebraic_of_rat: "algebraic (of_rat x)"
  by (rule algebraic_representsI[OF poly_rat_represents_of_rat])

lemma algebraic_uminus: "algebraic x  algebraic (-x)"
  by (auto dest: algebraic_imp_represents_irreducible intro: algebraic_representsI represents_uminus)

lemma algebraic_inverse: "algebraic x  algebraic (inverse x)"
  using algebraic_of_rat[of 0]
  by (cases "x = 0", auto dest: algebraic_imp_represents_irreducible intro: algebraic_representsI represents_inverse)

lemma algebraic_plus: "algebraic x  algebraic y  algebraic (x + y)"
  by (auto dest!: algebraic_imp_represents_irreducible_cf_pos intro!: algebraic_representsI[OF represents_add])

lemma algebraic_div:
  assumes x: "algebraic x" and y: "algebraic y" shows "algebraic (x/y)"
proof(cases "y = 0  x = 0")
  case True
  then show ?thesis using algebraic_of_rat[of 0] by auto
next
  case False
  then have x0: "x  0" and y0: "y  0" by auto
  from x y obtain p q
  where px: "p represents x" and irr: "irreducible q" and qy: "q represents y"
    by (auto dest!: algebraic_imp_represents_irreducible)
  show ?thesis
    using False px represents_irr_non_0[OF irr qy]
    by (auto intro!: algebraic_representsI[OF represents_div] qy)
qed

lemma algebraic_times: "algebraic x  algebraic y  algebraic (x * y)"
  using algebraic_div[OF _ algebraic_inverse, of x y] by (simp add: field_simps)

lemma algebraic_root: "algebraic x  algebraic (root n x)"
proof -
  assume "algebraic x"
  then obtain p where p: "p represents x" by (auto dest: algebraic_imp_represents_irreducible_cf_pos)
  from 
    algebraic_representsI[OF represents_nth_root_neg_real[OF _ this, of n]]
    algebraic_representsI[OF represents_nth_root_pos_real[OF _ this, of n]]
    algebraic_of_rat[of 0]
  show ?thesis by (cases "n = 0", force, cases "n > 0", force, cases "n < 0", auto)
qed

lemma algebraic_nth_root: "n  0  algebraic x  y^n = x  algebraic y"
  by (auto dest: algebraic_imp_represents_irreducible_cf_pos intro: algebraic_representsI represents_nth_root)

subsection ‹More on algebraic integers›

(* TODO: this is actually equal to @{term "(-1)^(m*n)"}, but we need a bit more theory on
   permutations to show this with a reasonable amount of effort. *)
definition poly_add_sign :: "nat  nat  'a :: comm_ring_1" where
  "poly_add_sign m n = signof (λi. if i < n then m + i else if i < m + n then i - n else i)"

lemma lead_coeff_poly_add:
  fixes p q :: "'a :: {idom, semiring_char_0} poly"
  defines "m  degree p" and "n  degree q"
  assumes "lead_coeff p = 1" "lead_coeff q = 1" "m > 0" "n > 0"
  shows "lead_coeff (poly_add p q :: 'a poly) = poly_add_sign m n"
proof -
  from assms have [simp]: "p  0" "q  0"
    by auto
  define M where "M = sylvester_mat (poly_x_minus_y p) (poly_lift q)"
  define π :: "nat  nat" where
    "π = (λi. if i < n then m + i else if i < m + n then i - n else i)"
  have π: "π permutes {0..<m+n}"
    by (rule inj_on_nat_permutes) (auto simp: π_def inj_on_def)
  have nz: "M $$ (i, π i)  0" if "i < m + n" for i
    using that by (auto simp: M_def π_def sylvester_index_mat m_def n_def)

(*
  have "{(i,j). i ∈ {..<m+n} ∧ j ∈ {..<m+n} ∧ i < j ∧ π i > π j} =
        {..<n} × {n..<m+n}" (is "?lhs = ?rhs")
  proof (intro equalityI subsetI)
    fix ij assume "ij ∈ ?lhs"
    thus "ij ∈ ?rhs"
      by (simp add: π_def split: prod.splits if_splits) auto
  qed (auto simp: π_def)
  hence "inversions_on {..<m+n} π = n * m"
    by (simp add: inversions_on_def)
  hence "signof π = (-1)^(m*n)"
    using π by (simp add: signof_def sign_def evenperm_iff_even_inversions)
*)

  have indices_eq: "{0..<m+n} = {..<n}  (+) n ` {..<m}"
    by (auto simp flip: atLeast0LessThan)

  define f where "f = (λ σ. signof σ * (i=0..<m+n. M $$ (i, σ i)))"
  have "degree (f π) = degree (i=0..<m + n. M $$ (i, π i))"
    using nz by (auto simp: f_def degree_mult_eq sign_def)
  also have " = (i=0..<m+n. degree (M $$ (i, π i)))"
    using nz by (subst degree_prod_eq_sum_degree) auto
  also have " = (i<n. degree (M $$ (i, π i))) + (i<m. degree (M $$ (n + i, π (n + i))))"
    by (subst indices_eq, subst sum.union_disjoint) (auto simp: sum.reindex)
  also have "(i<n. degree (M $$ (i, π i))) = (i<n. m)"
    by (intro sum.cong) (auto simp: M_def sylvester_index_mat π_def m_def n_def)
  also have "(i<m. degree (M $$ (n + i, π (n + i)))) = (i<m. 0)"
    by (intro sum.cong) (auto simp: M_def sylvester_index_mat π_def m_def n_def)
  finally have deg_f1: "degree (f π) = m * n"
    by simp

  have deg_f2: "degree (f σ) < m * n" if "σ permutes {0..<m+n}" "σ  π" for σ
  proof (cases "i{0..<m+n}. M $$ (i, σ i) = 0")
    case True
    hence *: "(i = 0..<m + n. M $$ (i, σ i)) = 0"
      by auto
    show ?thesis using m > 0 n > 0
      by (simp add: f_def *)
  next
    case False
    note nz = this
    from that have σ_less: "σ i < m + n" if "i < m + n" for i
      using permutes_in_image[OF σ permutes _] that by auto
    have "degree (f σ) = degree (i=0..<m + n. M $$ (i, σ i))"
      using nz by (auto simp: f_def degree_mult_eq sign_def)
    also have " = (i=0..<m+n. degree (M $$ (i, σ i)))"
      using nz by (subst degree_prod_eq_sum_degree) auto
    also have " = (i<n. degree (M $$ (i, σ i))) + (i<m. degree (M $$ (n + i, σ (n + i))))"
      by (subst indices_eq, subst sum.union_disjoint) (auto simp: sum.reindex)
    also have "(i<m. degree (M $$ (n + i, σ (n + i)))) = (i<m. 0)"
      using σ_less by (intro sum.cong) (auto simp: M_def sylvester_index_mat π_def m_def n_def)
    also have "(i<n. degree (M $$ (i, σ i))) < (i<n. m)"
    proof (rule sum_strict_mono_ex1)
      show "x{..<n}. degree (M $$ (x, σ x))  m" using σ_less
        by (auto simp: M_def sylvester_index_mat π_def m_def n_def degree_coeff_poly_x_minus_y)
    next

      have "i<n. σ i  π i"
      proof (rule ccontr)
        assume nex: "~(i<n. σ i  π i)"
        have "im+n-k. σ i = π i" if "k  m" for k
          using that
        proof (induction k)
          case 0
          thus ?case using π permutes _ σ permutes _
            by (fastforce simp: permutes_def)
        next
          case (Suc k)
          have IH: "σ i = π i" if "i  m+n-k" for i
            using Suc.prems Suc.IH that by auto
          from nz have "M $$ (m + n - Suc k, σ (m + n - Suc k))  0"
            using Suc.prems by auto
          moreover have "m + n - Suc k  n"
            using Suc.prems by auto
          ultimately have "σ (m+n-Suc k)  m-Suc k"
            using assms σ_less[of "m+n-Suc k"] Suc.prems
            by (auto simp: M_def sylvester_index_mat m_def n_def split: if_splits)
          have "¬(σ (m+n-Suc k) > m - Suc k)"
          proof
            assume *: "σ (m+n-Suc k) > m - Suc k"
            have less: "σ (m+n-Suc k) < m"
            proof (rule ccontr)
              assume *: "¬σ (m + n - Suc k) < m"
              define j where "j = σ (m + n - Suc k) - m"
              have "σ (m + n - Suc k) = m + j"
                using * by (simp add: j_def)
              moreover {
                have "j < n"
                  using σ_less[of "m+n-Suc k"] m > 0 n > 0 by (simp add: j_def)
                hence "σ j = π j"
                  using nex by auto
                with j < n have "σ j = m + j"
                  by (auto simp: π_def)
              }
              ultimately have "σ (m + n - Suc k) = σ j"
                by simp
              hence "m + n - Suc k = j"
                using permutes_inj[OF σ permutes _] unfolding inj_def by blast
              thus False using n  m + n - Suc k σ_less[of "m+n-Suc k"] n > 0 
                unfolding j_def by linarith
            qed
          
            define j where "j = σ (m+n-Suc k) - (m - Suc k)"
            from * have j: "σ (m+n-Suc k) = m - Suc k + j" "j > 0"
              by (auto simp: j_def)
            have "σ (m+n-Suc k + j) = π (m+n - Suc k + j)"
              using * by (intro IH) (auto simp: j_def)
            also {
              have "j < Suc k"
                using less by (auto simp: j_def algebra_simps)
              hence "m + n - Suc k + j < m + n"
                using m > 0 n > 0 Suc.prems by linarith
              hence "π (m +n - Suc k + j) = m - Suc k + j"
                unfolding π_def using Suc.prems by (simp add: π_def)
            }
            finally have "σ (m + n - Suc k + j) = σ (m + n - Suc k)"
              using j by simp
            hence "m + n - Suc k + j = m + n - Suc k"
              using permutes_inj[OF σ permutes _] unfolding inj_def by blast
            thus False using j > 0 by simp
          qed
          with σ (m+n-Suc k)  m-Suc k have eq: "σ (m+n-Suc k) = m - Suc k"
            by linarith

          show ?case
          proof safe
            fix i :: nat
            assume i: "i  m + n - Suc k"
            show "σ i = π i"
              using eq Suc.prems m > 0 IH i
            proof (cases "i = m + n - Suc k")
              case True
              thus ?thesis using eq Suc.prems m > 0
                by (auto simp: π_def)
            qed (use IH i in auto)
          qed
        qed
        from this[of m] and nex have "σ i = π i" for i
          by (cases "i  n") auto
        hence "σ = π" by force
        thus False using σ  π by contradiction
      qed

      then obtain i where i: "i < n" "σ i  π i"
        by auto
      have "σ i < m + n"
        using i by (intro σ_less) auto
      moreover have "π i = m + i"
        using i by (auto simp: π_def)
      ultimately have "degree (M $$ (i, σ i)) < m" using i m > 0
        by (auto simp: M_def m_def n_def sylvester_index_mat degree_coeff_poly_x_minus_y)
      thus "i{..<n}. degree (M $$ (i, σ i)) < m"
        using i by blast
    qed auto
    finally show "degree (f σ) < m * n"
      by (simp add: mult_ac)
  qed

  have "lead_coeff (f π) = poly_add_sign m n"
  proof -
    have "lead_coeff (f π) = signof π * (i=0..<m + n. lead_coeff (M $$ (i, π i)))"
      by (simp add: f_def sign_def lead_coeff_prod)
    also have "(i=0..<m + n. lead_coeff (M $$ (i, π i))) =
               (i<n. lead_coeff (M $$ (i, π i))) * (i<m. lead_coeff (M $$ (n + i, π (n + i))))"
      by (subst indices_eq, subst prod.union_disjoint) (auto simp: prod.reindex)
    also have "(i<n. lead_coeff (M $$ (i, π i))) = (i<n. lead_coeff p)"
      by (intro prod.cong) (auto simp: M_def m_def n_def π_def sylvester_index_mat)
    also have "(i<m. lead_coeff (M $$ (n + i, π (n + i)))) = (i<m. lead_coeff q)"
      by (intro prod.cong) (auto simp: M_def m_def n_def π_def sylvester_index_mat)
    also have "signof π = poly_add_sign m n"
      by (simp add: π_def poly_add_sign_def m_def n_def cong: if_cong)
    finally show ?thesis
      using assms by simp
  qed

  have "lead_coeff (poly_add p q) =
          lead_coeff (det (sylvester_mat (poly_x_minus_y p) (poly_lift q)))"
    by (simp add: poly_add_def resultant_def)
  also have "det (sylvester_mat (poly_x_minus_y p) (poly_lift q)) =
               (π | π permutes {0..<m+n}. f π)"
    by (simp add: det_def m_def n_def M_def f_def)
  also have "{π. π permutes {0..<m+n}} = insert π ({π. π permutes {0..<m+n}} - {π})"
    using π by auto
  also have "(σ. f σ) = (σ{σ. σ permutes {0..<m+n}}-{π}. f σ) + f π"
    by (subst sum.insert) (auto simp: finite_permutations)
  also have "lead_coeff  = lead_coeff (f π)"
  proof -
    have "degree (σ{σ. σ permutes {0..<m+n}}-{π}. f σ) < m * n" using assms
      by (intro degree_sum_smaller deg_f2) (auto simp: m_def n_def finite_permutations)
    with deg_f1 show ?thesis
      by (subst lead_coeff_add_le) auto
  qed
  finally show ?thesis
    using lead_coeff (f π) = _ by simp
qed

lemma lead_coeff_poly_mult:
  fixes p q :: "'a :: {idom, ring_char_0} poly"
  defines "m  degree p" and "n  degree q"
  assumes "lead_coeff p = 1" "lead_coeff q = 1" "m > 0" "n > 0"
  assumes "coeff q 0  0"
  shows "lead_coeff (poly_mult p q :: 'a poly) = 1"
proof -
  from assms have [simp]: "p  0" "q  0"
    by auto
  have [simp]: "degree (reflect_poly q) = n"
    using assms by (subst degree_reflect_poly_eq) (auto simp: n_def)

  define M where "M = sylvester_mat (poly_x_mult_y p) (poly_lift (reflect_poly q))"
  have nz: "M $$ (i, i)  0" if "i < m + n" for i
    using that by (auto simp: M_def sylvester_index_mat m_def n_def coeff_poly_x_mult_y)

  have indices_eq: "{0..<m+n} = {..<n}  (+) n ` {..<m}"
    by (auto simp flip: atLeast0LessThan)

  define f where "f = (λ σ. signof σ * (i=0..<m+n. M $$ (i, σ i)))"
  have "degree (f id) = degree (i=0..<m + n. M $$ (i, i))"
    using nz by (auto simp: f_def degree_mult_eq sign_def)
  also have " = (i=0..<m+n. degree (M $$ (i, i)))"
    using nz by (subst degree_prod_eq_sum_degree) auto
  also have " = (i<n. degree (M $$ (i, i))) + (i<m. degree (M $$ (n + i, n + i)))"
    by (subst indices_eq, subst sum.union_disjoint) (auto simp: sum.reindex)
  also have "(i<n. degree (M $$ (i, i))) = (i<n. m)"
    by (intro sum.cong)
       (auto simp: M_def sylvester_index_mat m_def n_def coeff_poly_x_mult_y degree_monom_eq)
  also have "(i<m. degree (M $$ (n + i, n + i))) = (i<m. 0)"
    by (intro sum.cong) (auto simp: M_def sylvester_index_mat m_def n_def)
  finally have deg_f1: "degree (f id) = m * n"
    by (simp add: mult_ac id_def)

  have deg_f2: "degree (f σ) < m * n" if "σ permutes {0..<m+n}" "σ  id" for σ
  proof (cases "i{0..<m+n}. M $$ (i, σ i) = 0")
    case True
    hence *: "(i = 0..<m + n. M $$ (i, σ i)) = 0"
      by auto
    show ?thesis using m > 0 n > 0
      by (simp add: f_def *)
  next
    case False
    note nz = this
    from that have σ_less: "σ i < m + n" if "i < m + n" for i
      using permutes_in_image[OF σ permutes _] that by auto
    have "degree (f σ) = degree (i=0..<m + n. M $$ (i, σ i))"
      using nz by (auto simp: f_def degree_mult_eq sign_def)
    also have " = (i=0..<m+n. degree (M $$ (i, σ i)))"
      using nz by (subst degree_prod_eq_sum_degree) auto
    also have " = (i<n. degree (M $$ (i, σ i))) + (i<m. degree (M $$ (n + i, σ (n + i))))"
      by (subst indices_eq, subst sum.union_disjoint) (auto simp: sum.reindex)
    also have "(i<m. degree (M $$ (n + i, σ (n + i)))) = (i<m. 0)"
      using σ_less by (intro sum.cong) (auto simp: M_def sylvester_index_mat m_def n_def)
    also have "(i<n. degree (M $$ (i, σ i))) < (i<n. m)"
    proof (rule sum_strict_mono_ex1)
      show "x{..<n}. degree (M $$ (x, σ x))  m" using σ_less
        by (auto simp: M_def sylvester_index_mat m_def n_def degree_coeff_poly_x_minus_y coeff_poly_x_mult_y
                 intro: order.trans[OF degree_monom_le])
    next
      have "i<n. σ i  i"
      proof (rule ccontr)
        assume nex: "¬(i<n. σ i  i)"
        have "σ i = i" for i
          using that
        proof (induction i rule: less_induct)
          case (less i)
          consider "i < n" | "i  {n..<m+n}" | "i  m + n"
            by force
          thus ?case
          proof cases
            assume "i < n"
            thus ?thesis using nex by auto
          next
            assume "i  m + n"
            thus ?thesis using σ permutes _
              by (auto simp: permutes_def)
          next
            assume i: "i  {n..<m+n}"
            have IH: "σ j = j" if "j < i" for j
              using that less.prems by (intro less.IH) auto

            from nz have "M $$ (i, σ i)  0"
              using i by auto
            hence "σ i  i"
              using i σ_less[of i] by (auto simp: M_def sylvester_index_mat m_def n_def)
            moreover have "σ i  i"
            proof (rule ccontr)
              assume *: "¬σ i  i"
              from * have "σ (σ i) = σ i"
                by (subst IH) auto
              hence "σ i = i"
                using permutes_inj[OF σ permutes _] unfolding inj_def by blast
              with * show False by simp
            qed
            ultimately show ?case by simp
          qed
        qed
        hence "σ = id"
          by force
        with σ  id show False
          by contradiction
      qed

      then obtain i where i: "i < n" "σ i  i"
        by auto
      have "σ i < m + n"
        using i by (intro σ_less) auto
      hence "degree (M $$ (i, σ i)) < m" using i m > 0
        by (auto simp: M_def m_def n_def sylvester_index_mat degree_coeff_poly_x_minus_y
                       coeff_poly_x_mult_y intro: le_less_trans[OF degree_monom_le])
      thus "i{..<n}. degree (M $$ (i, σ i)) < m"
        using i by blast
    qed auto
    finally show "degree (f σ) < m * n"
      by (simp add: mult_ac)
  qed

  have "lead_coeff (f id) = 1"
  proof -
    have "lead_coeff (f id) = (i=0..<m + n. lead_coeff (M $$ (i, i)))"
      by (simp add: f_def lead_coeff_prod)
    also have "(i=0..<m + n. lead_coeff (M $$ (i, i))) =
               (i<n. lead_coeff (M $$ (i, i))) * (i<m. lead_coeff (M $$ (n + i, n + i)))"
      by (subst indices_eq, subst prod.union_disjoint) (auto simp: prod.reindex)
    also have "(i<n. lead_coeff (M $$ (i, i))) = (i<n. lead_coeff p)" using assms
      by (intro prod.cong) (auto simp: M_def m_def n_def sylvester_index_mat
                                       coeff_poly_x_mult_y degree_monom_eq)
    also have "(i<m. lead_coeff (M $$ (n + i, n + i))) = (i<m. lead_coeff q)"
      by (intro prod.cong) (auto simp: M_def m_def n_def sylvester_index_mat)
    finally show ?thesis
      using assms by (simp add: id_def)
  qed

  have "lead_coeff (poly_mult p q) = lead_coeff (det M)"
    by (simp add: poly_mult_def resultant_def M_def poly_div_def)
  also have "det M = (π | π permutes {0..<m+n}. f π)"
    by (simp add: det_def m_def n_def M_def f_def)
  also have "{π. π permutes {0..<m+n}} = insert id ({π. π permutes {0..<m+n