# Theory Roots_Unity

theory Roots_Unity
imports Order_Polynomial Fundamental_Theorem_Algebra Ring_Hom_Poly
```(* author: Thiemann *)

section ‹Roots of Unity›

theory Roots_Unity
imports
Polynomial_Factorization.Order_Polynomial
"HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
Polynomial_Interpolation.Ring_Hom_Poly
begin

lemma cis_mult_cmod_id: "cis (arg x) * of_real (cmod x) = x"
using rcis_cmod_arg[unfolded rcis_def] by (simp add: ac_simps)

lemma rcis_mult_cis[simp]: "rcis n a * cis b = rcis n (a + b)" unfolding cis_rcis_eq rcis_mult by simp
lemma rcis_div_cis[simp]: "rcis n a / cis b = rcis n (a - b)" unfolding cis_rcis_eq rcis_divide by simp

lemma cis_plus_2pi[simp]: "cis (x + 2 * pi) = cis x" by (auto simp: complex_eq_iff)
lemma cis_plus_2pi_neq_1: assumes x: "0 < x" "x < 2 * pi"
shows "cis x ≠ 1"
proof -
from x have "cos x ≠ 1" by (smt cos_2pi_minus cos_monotone_0_pi cos_zero)
thus ?thesis by (auto simp: complex_eq_iff)
qed

lemma cis_times_2pi[simp]: "cis (of_nat n * 2 * pi) = 1"
proof (induct n)
case (Suc n)
have "of_nat (Suc n) * 2 * pi = of_nat n * 2 * pi + 2 * pi" by (simp add: distrib_right)
also have "cis … = 1" unfolding cis_plus_2pi Suc ..
finally show ?case .
qed simp

declare cis_pi[simp]

lemma cis_pi_2[simp]: "cis (pi / 2) = 𝗂"
by (auto simp: complex_eq_iff)

lemma cis_add_pi[simp]: "cis (pi + x) = - cis x"
by (auto simp: complex_eq_iff)

lemma cis_3_pi_2[simp]: "cis (pi * 3 / 2) = - 𝗂"
proof -
have "cis (pi * 3 / 2) = cis (pi + pi / 2)"
by (rule arg_cong[of _ _ cis], simp)
also have "… = - 𝗂" unfolding cis_add_pi by simp
finally show ?thesis .
qed

lemma rcis_plus_2pi[simp]: "rcis y (x + 2 * pi) = rcis y x" unfolding rcis_def by simp
lemma rcis_times_2pi[simp]: "rcis r (of_nat n * 2 * pi) = of_real r"
unfolding rcis_def cis_times_2pi by simp

lemma arg_rcis_cis: assumes n: "n > 0" shows "arg (rcis n x) = arg (cis x)"
using arg_bounded arg_unique cis_arg complex_mod_rcis n rcis_def sgn_eq by auto

lemma arg_eqD: assumes "arg (cis x) = arg (cis y)" "-pi < x" "x ≤ pi" "-pi < y" "y ≤ pi"
shows "x = y"
using assms(1) unfolding arg_unique[OF sgn_cis assms(2-3)] arg_unique[OF sgn_cis assms(4-5)] .

lemma rcis_inj_on: assumes r: "r ≠ 0" shows "inj_on (rcis r) {0 ..< 2 * pi}"
proof (rule inj_onI, goal_cases)
case (1 x y)
from arg_cong[OF 1(3), of "λ x. x / r"] have "cis x = cis y" using r by (simp add: rcis_def)
from arg_cong[OF this, of "λ x. inverse x"] have "cis (-x) = cis (-y)" by simp
from arg_cong[OF this, of uminus] have *: "cis (-x + pi) = cis (-y + pi)"
by (auto simp: complex_eq_iff)
have "- x + pi = - y + pi"
by (rule arg_eqD[OF arg_cong[OF *, of arg]], insert 1(1-2), auto)
thus ?case by simp
qed

lemma cis_inj_on: "inj_on cis {0 ..< 2 * pi}"
using rcis_inj_on[of 1] unfolding rcis_def by auto

definition root_unity :: "nat ⇒ 'a :: comm_ring_1 poly" where
"root_unity n = monom 1 n - 1"

lemma poly_root_unity: "poly (root_unity n) x = 0 ⟷ x^n = 1"
unfolding root_unity_def by (simp add: poly_monom)

lemma degree_root_unity[simp]: "degree (root_unity n) = n" (is "degree ?p = _")
proof -
have p: "?p = monom 1 n + (-1)" unfolding root_unity_def by auto
show ?thesis
proof (cases n)
case 0
thus ?thesis unfolding p by simp
next
case (Suc m)
show ?thesis unfolding p unfolding Suc
by (subst degree_add_eq_left, auto simp: degree_monom_eq)
qed
qed

lemma zero_root_unit[simp]: "root_unity n = 0 ⟷ n = 0" (is "?p = 0 ⟷ _")
proof (cases "n = 0")
case True
thus ?thesis unfolding root_unity_def by simp
next
case False
from degree_root_unity[of n] False
have "degree ?p ≠ 0" by auto
hence "?p ≠ 0" by fastforce
thus ?thesis using False by auto
qed

definition prod_root_unity :: "nat list ⇒ 'a :: idom poly" where
"prod_root_unity ns = prod_list (map root_unity ns)"

lemma poly_prod_root_unity: "poly (prod_root_unity ns) x = 0 ⟷ (∃k∈set ns. x ^ k = 1)"
unfolding prod_root_unity_def
by (simp add: poly_prod_list prod_list_zero_iff o_def image_def poly_root_unity)

lemma degree_prod_root_unity[simp]: "0 ∉ set ns ⟹ degree (prod_root_unity ns) = sum_list ns"
unfolding prod_root_unity_def
by (subst degree_prod_list_eq, auto simp: o_def)

lemma zero_prod_root_unit[simp]: "prod_root_unity ns = 0 ⟷ 0 ∈ set ns"
unfolding prod_root_unity_def prod_list_zero_iff by auto

lemma roots_of_unity: assumes n: "n ≠ 0"
shows "(λ i. (cis (of_nat i * 2 * pi / n))) ` {0 ..< n} = { x :: complex. x ^ n = 1}" (is "?prod = ?Roots")
"{x. poly (root_unity n) x = 0} = { x :: complex. x ^ n = 1}"
"card { x :: complex. x ^ n = 1} = n"
proof (atomize(full), goal_cases)
case 1
let ?one = "1 :: complex"
let ?p = "monom ?one n - 1"
have degM: "degree (monom ?one n) = n" by (rule degree_monom_eq, simp)
have "degree ?p = degree (monom ?one n + (-1))" by simp
also have "… = degree (monom ?one n)"
finally have degp: "degree ?p = n" unfolding degM .
with n have p: "?p ≠ 0" by auto
have roots: "?Roots = {x. poly ?p x = 0}"
unfolding poly_diff poly_monom by simp
also have "finite …" by (rule poly_roots_finite[OF p])
finally have fin: "finite ?Roots" .
have sub: "?prod ⊆ ?Roots"
proof
fix x
assume "x ∈ ?prod"
then obtain i where x: "x = cis (real i * 2 * pi / n)" by auto
have "x ^ n = cis (real i * 2 * pi)" unfolding x DeMoivre using n by simp
also have "… = 1" by simp
finally show "x ∈ ?Roots" by auto
qed
have Rn: "card ?Roots ≤ n" unfolding roots
by (rule poly_roots_degree[of ?p, unfolded degp, OF p])
have "… = card {0 ..< n}" by simp
also have "… = card ?prod"
proof (rule card_image[symmetric], rule inj_onI, goal_cases)
case (1 x y)
{
fix m
assume "m < n"
hence "real m < real n" by simp
from mult_strict_right_mono[OF this, of "2 * pi / real n"] n
have "real m * 2 * pi / real n < real n * 2 * pi / real n" by simp
hence "real m * 2 * pi / real n < 2 * pi" using n by simp
} note [simp] = this
have 0: "(1 :: real) ≠ 0" using n by auto
have "real x * 2 * pi / real n = real y * 2 * pi / real n"
by (rule inj_onD[OF rcis_inj_on 1(3)[unfolded cis_rcis_eq]], insert 1(1-2), auto)
with n show "x = y" by auto
qed
finally have cn:  "card ?prod = n" ..
with Rn have "card ?prod ≥ card ?Roots" by auto
with card_mono[OF fin sub] have card: "card ?prod = card ?Roots" by auto
have "?prod = ?Roots"
by (rule card_subset_eq[OF fin sub card])
from this roots[symmetric] cn[unfolded this]
show ?case unfolding root_unity_def by blast
qed

lemma poly_roots_dvd: fixes p :: "'a :: field poly"
assumes "p ≠ 0" and "degree p = n"
and "card {x. poly p x = 0} ≥ n" and "{x. poly p x = 0} ⊆ {x. poly q x = 0}"
shows "p dvd q"
proof -
from poly_roots_degree[OF assms(1)] assms(2-3) have "card {x. poly p x = 0} = n" by auto
from assms(1-2) this assms(4)
show ?thesis
proof (induct n arbitrary: p q)
case (0 p q)
from is_unit_iff_degree[OF 0(1)] 0(2) show ?case by blast
next
case (Suc n p q)
let ?P = "{x. poly p x = 0}"
let ?Q = "{x. poly q x = 0}"
from Suc(4-5) card_gt_0_iff[of ?P] obtain x where
x: "poly p x = 0" "poly q x = 0" and fin: "finite ?P" by auto
define r where "r = [:-x, 1:]"
from x[unfolded poly_eq_0_iff_dvd r_def[symmetric]] obtain p' q' where
p: "p = r * p'" and q: "q = r * q'" unfolding dvd_def by auto
from Suc(2) have "degree p = degree r + degree p'" unfolding p
by (subst degree_mult_eq, auto)
with Suc(3) have deg: "degree p' = n" unfolding r_def by auto
from Suc(2) p have p'0: "p' ≠ 0" by auto
let ?P' = "{x. poly p' x = 0}"
let ?Q' = "{x. poly q' x = 0}"
have P: "?P = insert x ?P'" unfolding p poly_mult unfolding r_def by auto
have Q: "?Q = insert x ?Q'" unfolding q poly_mult unfolding r_def by auto
{
assume "x ∈ ?P'"
hence "?P = ?P'" unfolding P by auto
from arg_cong[OF this, of card, unfolded Suc(4)] deg have False
using poly_roots_degree[OF p'0] by auto
} note xp' = this
hence xP': "x ∉ ?P'" by auto
have "card ?P = Suc (card ?P')" unfolding P
by (rule card_insert_disjoint[OF _ xP'], insert fin[unfolded P], auto)
with Suc(4) have card: "card ?P' = n" by auto
from Suc(5)[unfolded P Q] xP' have "?P' ⊆ ?Q'" by auto
from Suc(1)[OF p'0 deg card this]
have IH: "p' dvd q'" .
show ?case unfolding p q using IH by simp
qed
qed

lemma root_unity_decomp: assumes n: "n ≠ 0"
shows "root_unity n =
prod_list (map (λ i. [:-cis (of_nat i * 2 * pi / n), 1:]) [0 ..< n])" (is "?u = ?p")
proof -
have deg: "degree ?u = n" by simp
note main = roots_of_unity[OF n]
have dvd: "?u dvd ?p"
proof (rule poly_roots_dvd[OF _ deg])
show "n ≤ card {x. poly ?u x = 0}" using main by auto
show "?u ≠ 0" using n by auto
show "{x. poly ?u x = 0} ⊆ {x. poly ?p x = 0}"
unfolding main(2) main(1)[symmetric] poly_prod_list prod_list_zero_iff by auto
qed
have deg': "degree ?p = n"
by (subst degree_prod_list_eq, auto simp: o_def sum_list_triv)
have mon: "monic ?u" using deg unfolding root_unity_def using n by auto
have mon': "monic ?p" by (rule monic_prod_list, auto)
from dvd[unfolded dvd_def] obtain f where puf: "?p = ?u * f" by auto
have "degree ?p = degree ?u + degree f" using mon' n unfolding puf
by (subst degree_mult_eq, auto)
with deg deg' have "degree f = 0" by auto
from degree0_coeffs[OF this] obtain a where f: "f = [:a:]" by blast
from arg_cong[OF puf, of lead_coeff] mon mon'
have "a = 1" unfolding puf f by (cases "a = 0", auto)
with f have f: "f = 1" by auto
with puf show ?thesis by auto
qed

lemma order_monic_linear: "order x [:y,1:] = (if y + x = 0 then 1 else 0)"
proof (cases "y + x = 0")
case True
hence "poly [:y,1:] x = 0" by simp
from this[unfolded order_root] have "order x [:y,1:] ≠ 0" by auto
moreover from order_degree[of "[:y,1:]" x] have "order x [:y,1:] ≤ 1" by auto
ultimately show ?thesis unfolding True by auto
next
case False
hence "poly [:y,1:] x ≠ 0" by auto
from order_0I[OF this] False show ?thesis by auto
qed

lemma order_root_unity: fixes x :: complex assumes n: "n ≠ 0"
shows "order x (root_unity n) = (if x^n = 1 then 1 else 0)"
(is "order _ ?u = _")
proof (cases "x^n = 1")
case False
with roots_of_unity(2)[OF n] have "poly ?u x ≠ 0" by auto
from False order_0I[OF this] show ?thesis by auto
next
case True
let ?phi = "λ i :: nat. i * 2 * pi / n"
from True roots_of_unity(1)[OF n] obtain i where i: "i < n"
and x: "x = cis (?phi i)" by force
from i have n_split: "[0 ..< n] = [0 ..< i] @ i # [Suc i ..< n]"
by (metis le_Suc_ex less_imp_le_nat not_le_imp_less not_less0 upt_add_eq_append upt_conv_Cons)
{
fix j
assume j: "j < n ∨ j < i" and eq: "cis (?phi i) = cis (?phi j)"
from inj_onD[OF cis_inj_on eq] i j n have "i = j" by (auto simp: field_simps)
} note inj = this
have "order x ?u = 1" unfolding root_unity_decomp[OF n]
unfolding x n_split using inj
by (subst order_prod_list, force, fastforce simp: order_monic_linear)
with True show ?thesis by auto
qed

lemma order_prod_root_unity: assumes 0: "0 ∉ set ks"
shows "order (x :: complex) (prod_root_unity ks) = length (filter (λ k. x^k = 1) ks)"
proof -
have "order x (prod_root_unity ks) = (∑k←ks. order x (root_unity k))"
unfolding prod_root_unity_def
by (subst order_prod_list, insert 0, auto simp: o_def)
also have "… = (∑k←ks. (if x^k = 1 then 1 else 0))"
by (rule arg_cong, rule map_cong, insert 0, force, intro order_root_unity, metis)
also have "… = length (filter (λ k. x^k = 1) ks)"
by (subst sum_list_map_filter'[symmetric], simp add: sum_list_triv)
finally show ?thesis .
qed

lemma root_unity_witness: fixes xs :: "complex list"
assumes "prod_list (map (λ x. [:-x,1:]) xs) = monom 1 n - 1"
shows "x^n = 1 ⟷ x ∈ set xs"
proof -
from assms have n0: "n ≠ 0" by (cases "n = 0", auto simp: prod_list_zero_iff)
have "x ∈ set xs ⟷ poly (prod_list (map (λ x. [:-x,1:]) xs)) x = 0"
unfolding poly_prod_list prod_list_zero_iff by auto
also have "… ⟷ x^n = 1" using roots_of_unity(2)[OF n0] unfolding assms root_unity_def by auto
finally show ?thesis by auto
qed

lemma root_unity_explicit: fixes x :: complex
shows
"(x ^ 1 = 1) ⟷ x = 1"
"(x ^ 2 = 1) ⟷ (x ∈ {1, -1})"
"(x ^ 3 = 1) ⟷ (x ∈ {1, Complex (-1/2) (sqrt 3 / 2), Complex (-1/2) (- sqrt 3 / 2)})"
"(x ^ 4 = 1) ⟷ (x ∈ {1, -1, 𝗂, - 𝗂})"
proof -
show "(x ^ 1 = 1) ⟷ x = 1"
by (subst root_unity_witness[of ""], code_simp, auto)
show "(x ^ 2 = 1) ⟷ (x ∈ {1, -1})"
by (subst root_unity_witness[of "[1,-1]"], code_simp, auto)
show "(x ^ 4 = 1) ⟷ (x ∈ {1, -1, 𝗂, - 𝗂})"
by (subst root_unity_witness[of "[1,-1, 𝗂, - 𝗂]"], code_simp, auto)
have 3: "3 = Suc (Suc (Suc 0))" "1 = [:1:]" by auto
show "(x ^ 3 = 1) ⟷ (x ∈ {1, Complex (-1/2) (sqrt 3 / 2), Complex (-1/2) (- sqrt 3 / 2)})"
by (subst root_unity_witness[of
"[1, Complex (-1/2) (sqrt 3 / 2), Complex (-1/2) (- sqrt 3 / 2)]"],
auto simp: 3 monom_altdef complex_mult complex_eq_iff)
qed

definition primitive_root_unity :: "nat ⇒ 'a :: power ⇒ bool" where
"primitive_root_unity k x = (k ≠ 0 ∧ x^k = 1 ∧ (∀ k' < k. k' ≠ 0 ⟶ x^k' ≠ 1))"

lemma primitive_root_unityD: assumes "primitive_root_unity k x"
shows "k ≠ 0" "x^k = 1" "k' ≠ 0 ⟹ x^k' = 1 ⟹ k ≤ k'"
proof -
note * = assms[unfolded primitive_root_unity_def]
from * have **: "k' < k ⟹ k' ≠ 0 ⟹ x ^ k' ≠ 1" by auto
show "k ≠ 0" "x^k = 1" using * by auto
show "k' ≠ 0 ⟹ x^k' = 1 ⟹ k ≤ k'" using ** by force
qed

lemma primitive_root_unity_exists: assumes "k ≠ 0" "x ^ k = 1"
shows "∃ k'. k' ≤ k ∧ primitive_root_unity k' x"
proof -
let ?P = "λ k. x ^ k = 1 ∧ k ≠ 0"
define k' where "k' = (LEAST k. ?P k)"
from assms have Pk: "∃ k. ?P k" by auto
from LeastI_ex[OF Pk, folded k'_def]
have "k' ≠ 0" "x ^ k' = 1" by auto
with not_less_Least[of _ ?P, folded k'_def]
have "primitive_root_unity k' x" unfolding primitive_root_unity_def by auto
with primitive_root_unityD(3)[OF this assms]
show ?thesis by auto
qed

lemma primitive_root_unity_dvd: fixes x :: "complex"
assumes k: "primitive_root_unity k x"
shows "x ^ n = 1 ⟷ k dvd n"
proof
assume "k dvd n" then obtain j where n: "n = k * j" unfolding dvd_def by auto
have "x ^ n = (x ^ k) ^ j" unfolding n power_mult by simp
also have "… = 1" unfolding primitive_root_unityD[OF k] by simp
finally show "x ^ n = 1" .
next
assume n: "x ^ n = 1"
note k = primitive_root_unityD[OF k]
show "k dvd n"
proof (cases "n = 0")
case n0: False
from k(3)[OF n0] n have nk: "n ≥ k" by force
from roots_of_unity[OF k(1)] k(2) obtain i :: nat where xk: "x = cis (i * 2 * pi / k)"
and ik: "i < k" by force
from roots_of_unity[OF n0] n obtain j :: nat where xn: "x = cis (j * 2 * pi / n)"
and jn: "j < n" by force
have cop: "coprime i k"
proof (rule gcd_eq_1_imp_coprime)
from k(1) have "gcd i k ≠ 0" by auto
from gcd_coprime_exists[OF this] this obtain i' k' g where
*: "i = i' * g" "k = k' * g" "g ≠ 0" and g: "g = gcd i k" by blast
from *(2) k(1) have k': "k' ≠ 0" by auto
have "x = cis (i * 2 * pi / k)" by fact
also have "i * 2 * pi / k = i' * 2 * pi / k'" unfolding * using *(3) by auto
finally have "x ^ k' = 1" by (simp add: DeMoivre k')
with k(3)[OF k'] have "k' ≥ k" by linarith
moreover with * k(1) have "g = 1" by auto
then show "gcd i k = 1" by (simp add: g)
qed
from inj_onD[OF cis_inj_on xk[unfolded xn]] n0 k(1) ik jn
have "j * real k = i * real n" by (auto simp: field_simps)
hence "real (j * k) = real (i * n)" by simp
hence eq: "j * k = i * n" by linarith
with cop show "k dvd n"
by (metis coprime_commute coprime_dvd_mult_right_iff dvd_triv_right)
qed auto
qed

lemma primitive_root_unity_simple_computation:
"primitive_root_unity k x  = (if k = 0 then False else
x ^ k = 1 ∧ (∀ i ∈ {1 ..< k}. x ^ i ≠ 1))"
unfolding primitive_root_unity_def by auto

lemma primitive_root_unity_explicit: fixes x :: complex
shows "primitive_root_unity 1 x ⟷ x = 1"
"primitive_root_unity 2 x ⟷ x = -1"
"primitive_root_unity 3 x ⟷ (x ∈ {Complex (-1/2) (sqrt 3 / 2), Complex (-1/2) (- sqrt 3 / 2)})"
"primitive_root_unity 4 x ⟷ (x ∈ {𝗂, - 𝗂})"
proof (atomize(full), goal_cases)
case 1
{
fix P :: "nat ⇒ bool"
have *: "{1 ..< 2 :: nat} = {1}" "{1 ..< 3 :: nat} = {1,2}" "{1 ..< 4 :: nat} = {1,2,3}"
by code_simp+
have "(∀i∈ {1 ..< 2}. P i) = P 1" "(∀i∈ {1 ..< 3}. P i) ⟷ P 1 ∧ P 2"
"(∀i∈ {1 ..< 4}. P i) ⟷ P 1 ∧ P 2 ∧ P 3"
unfolding * by auto
} note * = this
show ?case unfolding primitive_root_unity_simple_computation root_unity_explicit *
by (auto simp: complex_eq_iff)
qed

function decompose_prod_root_unity_main ::
"'a :: field poly ⇒ nat ⇒ nat list × 'a poly" where
"decompose_prod_root_unity_main p k = (
if k = 0 then ([], p) else
let q = root_unity k in if q dvd p then if p = 0 then ([],0) else
map_prod (Cons k) id (decompose_prod_root_unity_main (p div q) k) else
decompose_prod_root_unity_main p (k - 1))"
by pat_completeness auto

termination by (relation "measure (λ (p,k). degree p + k)", auto simp: degree_div_less)

declare decompose_prod_root_unity_main.simps[simp del]

lemma decompose_prod_root_unity_main: fixes p :: "complex poly"
assumes p: "p = prod_root_unity ks * f"
and d: "decompose_prod_root_unity_main p k = (ks',g)"
and f: "⋀ x. cmod x = 1 ⟹ poly f x ≠ 0"
and k: "⋀ k'. k' > k ⟹ ¬ root_unity k' dvd p"
shows "p = prod_root_unity ks' * f ∧ f = g ∧ set ks = set ks'"
using d p k
proof (induct p k arbitrary: ks ks' rule: decompose_prod_root_unity_main.induct)
case (1 p k ks ks')
note p = 1(4)
note k = 1(5)
from k[of "Suc k"] have p0: "p ≠ 0" by auto
hence "p = 0 ⟷ False" by auto
note d = 1(3)[unfolded decompose_prod_root_unity_main.simps[of p k] this if_False Let_def]
from p0[unfolded p] have ks0: "0 ∉ set ks" by simp
from f[of 1] have f0: "f ≠ 0" by auto
note IH = 1(1)[OF _ refl _ p0] 1(2)[OF _ refl]
show ?case
proof (cases "k = 0")
case True
with p k[unfolded this, of "hd ks"] p0 have "ks = []"
by (cases ks, auto simp: prod_root_unity_def)
with d p True show ?thesis by (auto simp: prod_root_unity_def)
next
case k0: False
note IH = IH[OF k0]
from k0 have "k = 0 ⟷ False" by auto
note d = d[unfolded this if_False]
let ?u = "root_unity k :: complex poly"
show ?thesis
proof (cases "?u dvd p")
case True
note IH = IH(1)[OF True]
let ?call = "decompose_prod_root_unity_main (p div ?u) k"
from True d obtain Ks where rec: "?call = (Ks,g)" and ks': "ks' = (k # Ks)"
by (cases ?call, auto)
from True have "?u dvd p ⟷ True" by simp
note d = d[unfolded this if_True rec]
let ?x = "cis (2 * pi / k)"
have rt: "poly ?u ?x = 0" unfolding poly_root_unity using cis_times_2pi[of 1]
with True have "poly p ?x = 0" unfolding dvd_def by auto
from this[unfolded p] f[of ?x] rt have "poly (prod_root_unity ks) ?x = 0"
unfolding poly_root_unity by auto
from this[unfolded poly_prod_root_unity] ks0 obtain k' where k': "k' ∈ set ks"
and rt: "?x ^ k' = 1" and k'0: "k' ≠ 0" by auto
let ?u' = "root_unity k' :: complex poly"
from k' rt k'0 have rtk': "poly ?u' ?x = 0" unfolding poly_root_unity by auto
{
let ?phi = " k' * (2 * pi / k)"
assume "k' < k"
hence "0 < ?phi" "?phi < 2 * pi" using k0 k'0 by (auto simp: field_simps)
from cis_plus_2pi_neq_1[OF this] rtk'
have False unfolding poly_root_unity DeMoivre ..
}
hence kk': "k ≤ k'" by presburger
{
assume "k' > k"
from k[OF this, unfolded p]
have "¬ ?u' dvd prod_root_unity ks" using dvd_mult2 by auto
with k' have False unfolding prod_root_unity_def
using prod_list_dvd[of ?u' "map root_unity ks"] by auto
}
with kk' have kk': "k' = k" by presburger
with k' have "k ∈ set ks" by auto
from split_list[OF this] obtain ks1 ks2 where ks: "ks = ks1 @ k # ks2" by auto
hence "p div ?u = (?u * (prod_root_unity (ks1 @ ks2) * f)) div ?u"
by (simp add: ac_simps p prod_root_unity_def)
also have "… = prod_root_unity (ks1 @ ks2) * f"
by (rule nonzero_mult_div_cancel_left, insert k0, auto)
finally have id: "p div ?u = prod_root_unity (ks1 @ ks2) * f" .
from d have ks': "ks' = k # Ks" by auto
have "k < k' ⟹ ¬ root_unity k' dvd p div ?u" for k'
using k[of k'] True by (metis dvd_div_mult_self dvd_mult2)
from IH[OF rec id this]
have id: "p div root_unity k = prod_root_unity Ks * f" and
*: "f = g ∧ set (ks1 @ ks2) = set Ks" by auto
from arg_cong[OF id, of "λ x. x * ?u"] True
have "p = prod_root_unity Ks * f * root_unity k" by auto
thus ?thesis using * unfolding ks ks' by (auto simp: prod_root_unity_def)
next
case False
from d False have "decompose_prod_root_unity_main p (k - 1) = (ks',g)" by auto
note IH = IH(2)[OF False this p]
have k: "k - 1 < k' ⟹ ¬ root_unity k' dvd p" for k' using False k[of k'] k0
by (cases "k' = k", auto)
show ?thesis by (rule IH, insert False k, auto)
qed
qed
qed

definition "decompose_prod_root_unity p = decompose_prod_root_unity_main p (degree p)"

lemma decompose_prod_root_unity: fixes p :: "complex poly"
assumes p: "p = prod_root_unity ks * f"
and d: "decompose_prod_root_unity p = (ks',g)"
and f: "⋀ x. cmod x = 1 ⟹ poly f x ≠ 0"
and p0: "p ≠ 0"
shows "p = prod_root_unity ks' * f ∧ f = g ∧ set ks = set ks'"
proof (rule decompose_prod_root_unity_main[OF p d[unfolded decompose_prod_root_unity_def] f])
fix k
assume deg: "degree p < k"
hence "degree p < degree (root_unity k)" by simp
with p0 show "¬ root_unity k dvd p"
qed

lemma (in comm_ring_hom) hom_root_unity: "map_poly hom (root_unity n) = root_unity n"
proof -
interpret p: map_poly_comm_ring_hom hom ..
show ?thesis unfolding root_unity_def
qed

lemma (in idom_hom) hom_prod_root_unity: "map_poly hom (prod_root_unity n) = prod_root_unity n"
proof -
interpret p: map_poly_comm_ring_hom hom ..
show ?thesis unfolding prod_root_unity_def p.hom_prod_list map_map o_def hom_root_unity ..
qed

lemma (in field_hom) hom_decompose_prod_root_unity_main:
"decompose_prod_root_unity_main (map_poly hom p) k = map_prod id (map_poly hom)
(decompose_prod_root_unity_main p k)"
proof (induct p k rule: decompose_prod_root_unity_main.induct)
case (1 p k)
let ?h = "map_poly hom"
let ?p = "?h p"
let ?u = "root_unity k :: 'a poly"
let ?u' = "root_unity k :: 'b poly"
interpret p: map_poly_inj_idom_divide_hom hom ..
have u': "?u' = ?h ?u" unfolding hom_root_unity ..
note simp = decompose_prod_root_unity_main.simps
let ?rec1 = "decompose_prod_root_unity_main (p div ?u) k"
have 0: "?p = 0 ⟷ p = 0" by simp
show ?case
unfolding simp[of ?p k] simp[of p k] if_distrib[of "map_prod id ?h"] Let_def u'
unfolding 0 p.hom_div[symmetric] p.hom_dvd_iff
by (rule if_cong[OF refl], force, rule if_cong[OF refl if_cong[OF refl]], force,
(subst 1(1), auto, cases ?rec1, auto),
(subst 1(2), auto))
qed

lemma (in field_hom) hom_decompose_prod_root_unity:
"decompose_prod_root_unity (map_poly hom p) = map_prod id (map_poly hom)
(decompose_prod_root_unity p)"
unfolding decompose_prod_root_unity_def
by (subst hom_decompose_prod_root_unity_main, simp)

end
```