Quelle  Gauss_Sums.thy

(*
  File:     Gauss_Sums.thy
  Authors:  Rodrigo Raya, EPFL; Manuel Eberl, TUM

  Gauss sums and more on Dirichlet characters: induced moduli, separability, primitive characters
*)
theory Gauss_Sums
imports 
  "HOL-Algebra.Coset"
  "HOL-Real_Asymp.Real_Asymp"
  Ramanujan_Sums
begin

section ‹Gauss sums›

bundle vec_lambda_syntax
begin
notation vec_lambda (binder ‹χ› 10)
end

unbundle no vec_lambda_syntax


subsection ‹Definition and basic properties›
context dcharacter
begin                            

(* TODO remove when integrating periodic and periodic_function *)
lemma dir_periodic_arithmetic: "periodic_arithmetic χ n"
  unfolding periodic_arithmetic_def by (simp add: periodic)

definition "gauss_sum k = (∑m = 1..n . χ(m) * unity_root n (m*k))"

lemma gauss_sum_periodic: 
  "periodic_arithmetic (λn. gauss_sum n) n"
proof - 
  have "periodic_arithmetic χ n" using dir_periodic_arithmetic by simp
  let ?h = "λm k. χ(m) * unity_root n (m*k)"
  {fix m :: nat
  have "periodic_arithmetic (λk. unity_root n (m*k)) n"
    using unity_periodic_arithmetic_mult[of n m] by simp
  have "periodic_arithmetic (?h m) n" 
    using scalar_mult_periodic_arithmetic[OF ‹periodic_arithmetic (λk. unity_root n (m*k)) n›]
    by blast}
  then have per_all: "∀m ∈ {1..n}. periodic_arithmetic (?h m) n" by blast
  have "periodic_arithmetic (λk. (∑m = 1..n . χ(m) * unity_root n (m*k))) n" 
    using fin_sum_periodic_arithmetic_set[OF per_all] by blast
  then show ?thesis
    unfolding gauss_sum_def by blast
qed

lemma ramanujan_sum_conv_gauss_sum:
  assumes "χ = principal_dchar n"
  shows "ramanujan_sum n k = gauss_sum k" 
proof -
  {fix m
  from assms  
    have 1: "coprime m n ==> χ(m) = 1" and
         2: "¬ coprime m n ==> χ(m) = 0"  
      unfolding principal_dchar_def by auto}
  note eq = this

  have "gauss_sum k = (∑m = 1..n . χ(m) * unity_root n (m*k))"
    unfolding gauss_sum_def by simp
  also have "… = (∑m | m ∈ {1..n} ∧ coprime m n . χ(m) * unity_root n (m*k))"
    by (rule sum.mono_neutral_right,simp,blast,simp add: eq) 
  also have "… = (∑m | m ∈ {1..n} ∧ coprime m n . unity_root n (m*k))"
    by (simp add: eq)
  also have "… = ramanujan_sum n k" unfolding ramanujan_sum_def by blast
  finally show ?thesis ..
qed

lemma cnj_mult_self:
  assumes "coprime k n"
  shows "cnj (χ k) * χ k = 1"
proof -
  have "cnj (χ k) * χ k = norm (χ k)^2"
    by (simp add: mult.commute complex_mult_cnj cmod_def)
  also have "… = 1" 
    using norm[of k] assms by simp
  finally show ?thesis .
qed

text ‹Theorem 8.9›
theorem gauss_sum_reduction:
  assumes "coprime k n" 
  shows "gauss_sum k = cnj (χ k) * gauss_sum 1"
proof -
  from n have n_pos: "n > 0" by simp
  have "gauss_sum k = (∑r = 1..n . χ(r) * unity_root n (r*k))"
    unfolding gauss_sum_def by simp
  also have "… = (∑r = 1..n . cnj (χ(k)) * χ k * χ r * unity_root n (r*k))"
    using assms by (intro sum.cong) (auto simp: cnj_mult_self)
  also have "… = (∑r = 1..n . cnj (χ(k)) * χ (k*r) * unity_root n (r*k))"
    by (intro sum.cong) auto
  also have "… = cnj (χ(k)) * (∑r = 1..n . χ (k*r) * unity_root n (r*k))"
    by (simp add: sum_distrib_left algebra_simps)
  also have "…= cnj (χ(k)) * (∑r = 1..n . χ r * unity_root n r)"
  proof -
    have 1: "periodic_arithmetic (λr. χ r * unity_root n r) n"
      using dir_periodic_arithmetic unity_periodic_arithmetic mult_periodic_arithmetic by blast
    have "(∑r = 1..n . χ (k*r) * unity_root n (r*k)) =
          (∑r = 1..n . χ (r)* unity_root n r)"
      using periodic_arithmetic_remove_homothecy[OF assms(1) 1 n_pos]
      by (simp add: algebra_simps n)
    then show ?thesis by argo
  qed
  also have "… = cnj (χ(k)) * gauss_sum 1" 
    using gauss_sum_def by simp
  finally show ?thesis .
qed


text ‹
 The following variant takes an integer argument instead.
 ›
definition "gauss_sum_int k = (∑m=1..n. χ m * unity_root n (int m*k))"

sublocale gauss_sum_int: periodic_fun_simple gauss_sum_int "int n"
proof
  fix k
  show "gauss_sum_int (k + int n) = gauss_sum_int k"
    by (simp add: gauss_sum_int_def ring_distribs unity_root_add)
qed

lemma gauss_sum_int_cong:
  assumes "[a = b] (mod int n)"
  shows   "gauss_sum_int a = gauss_sum_int b"
proof -
  from assms obtain k where k: "b = a + int n * k"
    by (subst (asm) cong_iff_lin) auto
  thus ?thesis
    using gauss_sum_int.plus_of_int[of a k] by (auto simp: algebra_simps)
qed

lemma gauss_sum_conv_gauss_sum_int:
  "gauss_sum k = gauss_sum_int (int k)" 
  unfolding gauss_sum_def gauss_sum_int_def by auto

lemma gauss_sum_int_conv_gauss_sum:
  "gauss_sum_int k = gauss_sum (nat (k mod n))"
proof -
  have "gauss_sum (nat (k mod n)) = gauss_sum_int (int (nat (k mod n)))"
    by (simp add: gauss_sum_conv_gauss_sum_int)
  also have "… = gauss_sum_int k"
    using n
    by (intro gauss_sum_int_cong) (auto simp: cong_def)
  finally show ?thesis ..
qed

lemma gauss_int_periodic: "periodic_arithmetic gauss_sum_int n" 
  unfolding periodic_arithmetic_def gauss_sum_int_conv_gauss_sum by simp

proposition dcharacter_fourier_expansion:
  "χ m = (∑k=1..n. 1 / n * gauss_sum_int (-k) * unity_root n (m*k))"
proof -
  define g where "g = (λx. 1 / of_nat n *
      (∑m<n. χ m * unity_root n (- int x * int m)))"
  have per: "periodic_arithmetic χ n" using dir_periodic_arithmetic by simp
  have "χ m = (∑k<n. g k * unity_root n (m * int k))"
    using fourier_expansion_periodic_arithmetic(2)[OF _ per, of m] n by (auto simp: g_def)
  also have "… = (∑k = 1..n. g k * unity_root n (m * int k))"
  proof -
    have g_per: "periodic_arithmetic g n"
      using fourier_expansion_periodic_arithmetic(1)[OF _ per] n by (simp add: g_def)
    have fact_per: "periodic_arithmetic (λk. g k * unity_root n (int m * int k)) n"
      using mult_periodic_arithmetic[OF g_per] unity_periodic_arithmetic_mult by auto
    show ?thesis
    proof -
      have "(∑k<n. g k * unity_root n (int m * int k)) =
            (∑l = 0..n - Suc 0. g l * unity_root n (int m * int l))"
        using n by (intro sum.cong) auto
      also have "… = (∑l = Suc 0..n. g l * unity_root n (int m * int l))"
        using periodic_arithmetic_sum_periodic_arithmetic_shift[OF fact_per, of 1] n by auto
      finally show ?thesis by simp
    qed
  qed
  also have "… = (∑k = 1..n. (1 / of_nat n) * gauss_sum_int (-k) * unity_root n (m*k))"
  proof -
    {fix k :: nat
    have shift: "(∑m<n. χ m * unity_root n (- int k * int m)) =
        (∑m = 1..n. χ m * unity_root n (- int k * int m))"
    proof -
      have per_unit: "periodic_arithmetic (λm. unity_root n (- int k * int m)) n"
        using unity_periodic_arithmetic_mult by blast
      then have prod_per: "periodic_arithmetic (λm. χ m * unity_root n (- int k * int m)) n"
        using per mult_periodic_arithmetic by blast
      show ?thesis
      proof -
        have "(∑m<n. χ m * unity_root n (- int k * int m)) =
              (∑l = 0..n - Suc 0. χ l * unity_root n (- int k * int l))"
          using n by (intro sum.cong) auto
        also have "… = (∑m = 1..n. χ m * unity_root n (- int k * int m))"
          using periodic_arithmetic_sum_periodic_arithmetic_shift[OF prod_per, of 1] n by auto
        finally show ?thesis by simp
      qed
    qed
    have "g k = 1 / of_nat n *
      (∑m<n. χ m * unity_root n (- int k * int m))"
      using g_def by auto
    also have "… = 1 / of_nat n *
      (∑m = 1..n. χ m * unity_root n (- int k * int m))"
      using shift by simp
    also have "… = 1 / of_nat n * gauss_sum_int (-k)"
      unfolding gauss_sum_int_def 
      by (simp add: algebra_simps)
    finally have "g k = 1 / of_nat n * gauss_sum_int (-k)" by simp} 
    note g_expr = this
      show ?thesis
        by (rule sum.cong, simp, simp add: g_expr) 
    qed
    finally show ?thesis by auto
qed


subsection ‹Separability›

definition "separable k ⟷ gauss_sum k = cnj (χ k) * gauss_sum 1"

corollary gauss_coprime_separable:
  assumes "coprime k n" 
  shows   "separable k" 
  using gauss_sum_reduction[OF assms] unfolding separable_def by simp

text ‹Theorem 8.10›
theorem global_separability_condition:
  "(∀n>0. separable n) ⟷ (∀k>0. ¬coprime k n ⟶ gauss_sum k = 0)"
proof -
  {fix k 
  assume "¬ coprime k n"
  then have "χ(k) = 0" by (simp add: eq_zero)
  then have "cnj (χ k) = 0" by blast
  then have "separable k ⟷ gauss_sum k = 0" 
    unfolding separable_def by auto} 
  note not_case = this
  
  show ?thesis
    using gauss_coprime_separable not_case separable_def by blast      
qed

lemma of_real_moebius_mu [simp]: "of_real (moebius_mu k) = moebius_mu k"
  by (simp add: moebius_mu_def)

corollary principal_not_totally_separable:
  assumes "χ = principal_dchar n"
  shows "¬(∀k > 0. separable k)"
proof -
  have n_pos: "n > 0" using n by simp  
  have tot_0: "totient n ≠ 0" by (simp add: n_pos)
  have "moebius_mu (n div gcd n n) ≠ 0" by (simp add: ‹n > 0›)
  then have moeb_0: "∃k. moebius_mu (n div gcd k n) ≠ 0" by blast
  
  have lem: "gauss_sum k = totient n * moebius_mu (n div gcd k n) / totient (n div gcd k n)"
    if "k > 0" for k
  proof -
    have "gauss_sum k = ramanujan_sum n k"
      using ramanujan_sum_conv_gauss_sum[OF assms(1)] ..
    also have "… = totient n * moebius_mu (n div gcd k n) / (totient (n div gcd k n))"
      by (simp add: ramanujan_sum_k_n_dirichlet_expr[OF n_pos that])
    finally show ?thesis .
  qed
  have 2: "¬ coprime n n" using n by auto
  have 3: "gauss_sum n ≠ 0" 
    using lem[OF n_pos] tot_0 moebius_mu_1 by simp
  from n_pos 2 3 have
    "∃k>0. ¬coprime k n ∧ gauss_sum k ≠ 0" by blast
  then obtain k where "k > 0 ∧ ¬ coprime k n ∧ gauss_sum k ≠ 0" by blast
  note right_not_zero = this

  have "cnj (χ k) * gauss_sum 1 = 0" if "¬coprime k n" for k
    using that assms by (simp add: principal_dchar_def)
  then show ?thesis 
     unfolding separable_def using right_not_zero by auto
qed

text ‹Theorem 8.11›
theorem gauss_sum_1_mod_square_eq_k: 
  assumes "(∀k. k > 0 ⟶ separable k)" 
  shows "norm (gauss_sum 1) ^ 2 = real n" 
proof -
  have "(norm (gauss_sum 1))^2 = gauss_sum 1 * cnj (gauss_sum 1)"
    using complex_norm_square by blast
  also have "… = gauss_sum 1 * (∑m = 1..n. cnj (χ(m)) * unity_root n (-m))"
  proof -
    have "cnj (gauss_sum 1) = (∑m = 1..n. cnj (χ(m)) * unity_root n (-m))"
      unfolding gauss_sum_def by (simp add: unity_root_uminus)
    then show ?thesis by argo
  qed
  also have "… = (∑m = 1..n. gauss_sum 1 * cnj (χ(m)) * unity_root n (-m))"
    by (subst sum_distrib_left)(simp add: algebra_simps)
  also have "… = (∑m = 1..n. gauss_sum m * unity_root n (-m))"
  proof (rule sum.cong,simp)   
    fix x
    assume as: "x ∈ {1..n}"
    show "gauss_sum 1 * cnj (χ x) * unity_root n (-x) =
          gauss_sum x * unity_root n (-x)"
      using assms(1) unfolding separable_def 
      by (rule allE[of _ x]) (use as in auto)
  qed
  also have "… = (∑m = 1..n. (∑r = 1..n. χ r * unity_root n (r*m) * unity_root n (-m)))"
    unfolding gauss_sum_def 
    by (rule sum.cong,simp,rule sum_distrib_right)
  also have "… = (∑m = 1..n. (∑r = 1..n. χ r * unity_root n (m*(r-1)) ))"
    by (intro sum.cong refl) (auto simp: unity_root_diff of_nat_diff unity_root_uminus field_simps)
  also have "… = (∑r=1..n. (∑m=1..n. χ(r) *unity_root n (m*(r-1))))"
    by (rule sum.swap)
  also have "… = (∑r=1..n. χ(r) *(∑m=1..n. unity_root n (m*(r-1))))"
    by (rule sum.cong, simp, simp add: sum_distrib_left)
  also have "… = (∑r=1..n. χ(r) * unity_root_sum n (r-1))" 
  proof (intro sum.cong refl)
    fix x
    assume "x ∈ {1..n}" 
    then have 1: "periodic_arithmetic (λm. unity_root n (int (m * (x - 1)))) n"
      using unity_periodic_arithmetic_mult[of n "x-1"] 
      by (simp add: mult.commute)
    have "(∑m = 1..n. unity_root n (int (m * (x - 1)))) =
          (∑m = 0..n-1. unity_root n (int (m * (x - 1))))"
      using periodic_arithmetic_sum_periodic_arithmetic_shift[OF 1 _, of 1] n by simp
    also have "… = unity_root_sum n (x-1)"
      using n unfolding unity_root_sum_def by (intro sum.cong) (auto simp: mult_ac)
    finally have "(∑m = 1..n. unity_root n (int (m * (x - 1)))) =
                  unity_root_sum n (int (x - 1))" .
    then show "χ x * (∑m = 1..n. unity_root n (int (m * (x - 1)))) =
               χ x * unity_root_sum n (int (x - 1))" by argo
  qed
  also have "… = (∑r ∈ {1}. χ r * unity_root_sum n (int (r - 1)))"    
    using n unity_root_sum_nonzero_iff int_ops(6)
    by (intro sum.mono_neutral_right) auto
  also have "… = χ 1 * n" using n by simp 
  also have "… = n" by simp
  finally show ?thesis
    using of_real_eq_iff by fastforce
qed

text ‹Theorem 8.12›
theorem gauss_sum_nonzero_noncoprime_necessary_condition:
  assumes "gauss_sum k ≠ 0" "¬coprime k n" "k > 0"
  defines "d ≡ n div gcd k n"  
  assumes "coprime a n" "[a = 1] (mod d)" 
  shows   "d dvd n" "d < n" "χ a = 1" 
proof -
  show "d dvd n" 
    unfolding d_def using n by (subst div_dvd_iff_mult) auto
  from assms(2) have "gcd k n ≠ 1" by blast
  then have "gcd k n > 1" using assms(3,4) by (simp add: nat_neq_iff)
  with n show "d < n" by (simp add: d_def)

  have "periodic_arithmetic (λr. χ (r)* unity_root n (k*r)) n" 
    using mult_periodic_arithmetic[OF dir_periodic_arithmetic unity_periodic_arithmetic_mult] by auto
  then have 1: "periodic_arithmetic (λr. χ (r)* unity_root n (r*k)) n" 
    by (simp add: algebra_simps)
  
  have "gauss_sum k = (∑m = 1..n . χ(m) * unity_root n (m*k))"
    unfolding gauss_sum_def by blast
  also have "… = (∑m = 1..n . χ(m*a) * unity_root n (m*a*k))"
    using periodic_arithmetic_remove_homothecy[OF assms(5) 1] n by auto
  also have "… = (∑m = 1..n . χ(m*a) * unity_root n (m*k))"  
  proof (intro sum.cong refl)
    fix m
    from assms(6) obtain b where "a = 1 + b*d" 
      using ‹d < n› assms(5) cong_to_1'_nat by auto
    then have "m*a*k = m*k+m*b*(n div gcd k n)*k"
      by (simp add: algebra_simps d_def)
    also have "… = m*k+m*b*n*(k div gcd k n)"
      by (simp add: div_mult_swap dvd_div_mult)
    also obtain p where "… = m*k+m*b*n*p" by blast
    finally have "m*a*k = m*k+m*b*p*n" by simp
    then have 1: "m*a*k mod n= m*k mod n" 
      using mod_mult_self1 by simp
    then have "unity_root n (m * a * k) = unity_root n (m * k)" 
    proof -
      have "unity_root n (m * a * k) = unity_root n ((m * a * k) mod n)"
        using unity_root_mod[of n] zmod_int by simp
      also have "… = unity_root n (m * k)" 
        using unity_root_mod[of n] zmod_int 1 by presburger
      finally show ?thesis by blast
    qed
    then show "χ (m * a) * unity_root n (int (m * a * k)) =
               χ (m * a) * unity_root n (int (m * k))" by auto
  qed
  also have "… = (∑m = 1..n . χ(a) * (χ(m) * unity_root n (m*k)))"
    by (rule sum.cong,simp,subst mult,simp)
  also have "… = χ(a) * (∑m = 1..n . χ(m) * unity_root n (m*k))"
    by (simp add: sum_distrib_left[symmetric]) 
  also have "… = χ(a) * gauss_sum k" 
    unfolding gauss_sum_def by blast
  finally have "gauss_sum k = χ(a) * gauss_sum k" by blast
  then show "χ a = 1" 
    using assms(1) by simp
qed


subsection ‹Induced moduli and primitive characters›

definition "induced_modulus d ⟷ d dvd n ∧ (∀a. coprime a n ∧ [a = 1] (mod d) ⟶ χ a = 1)"

lemma induced_modulus_dvd: "induced_modulus d ==> d dvd n"
  unfolding induced_modulus_def by blast

lemma induced_modulusI [intro?]:
  "d dvd n ==> (∧a. coprime a n ==> [a = 1] (mod d) ==> χ a = 1) ==> induced_modulus d"
  unfolding induced_modulus_def by auto

lemma induced_modulusD: "induced_modulus d ==> coprime a n ==> [a = 1] (mod d) ==> χ a = 1"
  unfolding induced_modulus_def by blast

lemma zero_not_ind_mod: "¬induced_modulus 0" 
  unfolding induced_modulus_def using n by simp

lemma div_gcd_dvd1: "(a :: 'a :: semiring_gcd) div gcd a b dvd a"
  by (metis dvd_def dvd_div_mult_self gcd_dvd1)

lemma div_gcd_dvd2: "(b :: 'a :: semiring_gcd) div gcd a b dvd b"
  by (metis div_gcd_dvd1 gcd.commute)

lemma g_non_zero_ind_mod:
  assumes "gauss_sum k ≠ 0" "¬coprime k n" "k > 0"
  shows  "induced_modulus (n div gcd k n)"
proof
  show "n div gcd k n dvd n"
    by (metis dvd_div_mult_self dvd_triv_left gcd.commute gcd_dvd1)
  fix a :: nat
  assume "coprime a n" "[a = 1] (mod n div gcd k n)"
  thus "χ a = 1"
    using assms n gauss_sum_nonzero_noncoprime_necessary_condition(3) by auto
qed

lemma induced_modulus_modulus: "induced_modulus n"
  unfolding induced_modulus_def
  by (metis dvd_refl local.cong mult.one) 

text ‹Theorem 8.13›
theorem one_induced_iff_principal:
 "induced_modulus 1 ⟷ χ = principal_dchar n"
proof
  assume "induced_modulus 1" 
  then have "(∀a. coprime a n ⟶ χ a = 1)"
    unfolding induced_modulus_def by simp
  then show "χ = principal_dchar n" 
    unfolding principal_dchar_def using eq_zero by auto
next
  assume as: "χ = principal_dchar n"
  {fix a
  assume "coprime a n"
  then have "χ a = 1" 
    using principal_dchar_def as by simp}
  then show "induced_modulus 1"
    unfolding induced_modulus_def by auto
qed

end


locale primitive_dchar = dcharacter +
  assumes no_induced_modulus: "¬(∃d<n. induced_modulus d)"

locale nonprimitive_dchar = dcharacter +
  assumes induced_modulus: "∃d<n. induced_modulus d"

lemma (in nonprimitive_dchar) nonprimitive: "¬primitive_dchar n χ"
proof
  assume "primitive_dchar n χ"
  then interpret A: primitive_dchar n "residue_mult_group n" χ
    by auto
  from A.no_induced_modulus induced_modulus show False by contradiction
qed

lemma (in dcharacter) primitive_dchar_iff:
  "primitive_dchar n χ ⟷ ¬(∃d<n. induced_modulus d)"
  unfolding primitive_dchar_def primitive_dchar_axioms_def
  using dcharacter_axioms by metis

lemma (in residues_nat) principal_not_primitive: 
  "¬primitive_dchar n (principal_dchar n)"
  unfolding principal.primitive_dchar_iff
  using principal.one_induced_iff_principal n by auto

lemma (in dcharacter) not_primitive_imp_nonprimitive:
  assumes "¬primitive_dchar n χ"
  shows   "nonprimitive_dchar n χ"
  using assms dcharacter_axioms
  unfolding nonprimitive_dchar_def primitive_dchar_def
            primitive_dchar_axioms_def nonprimitive_dchar_axioms_def by auto


text ‹Theorem 8.14›
theorem (in dcharacter) prime_nonprincipal_is_primitive:
  assumes "prime n"
  assumes "χ ≠ principal_dchar n" 
  shows   "primitive_dchar n χ"
proof -
  {fix m
  assume "induced_modulus m" 
  then have "m = n" 
    using assms prime_nat_iff induced_modulus_def
          one_induced_iff_principal by blast}
  then show ?thesis using primitive_dchar_iff by blast
qed

text ‹Theorem 8.15›
corollary (in primitive_dchar) primitive_encoding:
  "∀k>0. ¬coprime k n ⟶ gauss_sum k = 0" 
  "∀k>0. separable k"
  "norm (gauss_sum 1) ^ 2 = n"
proof safe
  show 1: "gauss_sum k = 0" if "k > 0" and "¬coprime k n" for k
  proof (rule ccontr)
    assume "gauss_sum k ≠ 0"
    hence "induced_modulus (n div gcd k n)"
      using that by (intro g_non_zero_ind_mod) auto
    moreover have "n div gcd k n < n"
      using n that
      by (meson coprime_iff_gcd_eq_1 div_eq_dividend_iff le_less_trans
                linorder_neqE_nat nat_dvd_not_less principal.div_gcd_dvd2 zero_le_one)
    ultimately show False using no_induced_modulus by blast
  qed

  have "(∀n>0. separable n)"
    unfolding global_separability_condition by (auto intro!: 1)
  thus "separable n" if "n > 0" for n
    using that by blast
  thus "norm (gauss_sum 1) ^ 2 = n"
    using gauss_sum_1_mod_square_eq_k by blast
qed

text ‹Theorem 8.16›
lemma (in dcharacter) induced_modulus_altdef1:
  "induced_modulus d ⟷
     d dvd n ∧ (∀a b. coprime a n ∧ coprime b n ∧ [a = b] (mod d) ⟶ χ a = χ b)"
proof 
  assume 1: "induced_modulus d"
  with n have d: "d dvd n" "d > 0"
    by (auto simp: induced_modulus_def intro: Nat.gr0I)
  show " d dvd n ∧ (∀a b. coprime a n ∧ coprime b n ∧ [a = b] (mod d) ⟶ χ(a) = χ(b))"
  proof safe
    fix a b
    assume 2: "coprime a n" "coprime b n" "[a = b] (mod d)"
    show "χ(a) = χ(b)" 
    proof -
      from 2(1) obtain a' where eq: "[a*a' = 1] (mod n)"
        using cong_solve by blast
      from this d have "[a*a' = 1] (mod d)"
        using cong_dvd_modulus_nat by blast
      from this 1 have "χ(a*a') = 1" 
        unfolding induced_modulus_def
        by (meson "2"(2) eq cong_imp_coprime cong_sym coprime_divisors gcd_nat.refl one_dvd)
      then have 3: "χ(a)*χ(a') = 1" 
        by simp

      from 2(3) have "[a*a' = b*a'] (mod d)" 
        by (simp add: cong_scalar_right)
      moreover have 4: "[b*a' = 1] (mod d)" 
        using ‹[a * a' = 1] (mod d)› calculation cong_sym cong_trans by blast
      have "χ(b*a') = 1" 
      proof -
        have "coprime (b*a') n"
          using "2"(2) cong_imp_coprime[OF cong_sym[OF eq]] by simp
        then show ?thesis using 4 induced_modulus_def 1 by blast
      qed
      then have 4: "χ(b)*χ(a') = 1" 
        by simp
      from 3 4 show "χ(a) = χ(b)" 
        using mult_cancel_left
        by (cases "χ(a') = 0") (fastforce simp add: field_simps)+
    qed
  qed fact+
next 
  assume *: "d dvd n ∧ (∀a b. coprime a n ∧ coprime b n ∧ [a = b] (mod d) ⟶ χ a = χ b)"
  then have "∀a . coprime a n ∧ coprime 1 n ∧ [a = 1] (mod d) ⟶ χ a = χ 1"
    by blast
  then have "∀a . coprime a n ∧ [a = 1] (mod d) ⟶ χ a = 1"
    using coprime_1_left by simp
  then show "induced_modulus d"
    unfolding induced_modulus_def using * by blast
qed

text ‹Exercise 8.4›

lemma induced_modulus_altdef2_lemma:
  fixes n a d q :: nat
  defines "q ≡ (∏ p | prime p ∧ p dvd n ∧ ¬ (p dvd a). p)"
  defines "m ≡ a + q * d"
  assumes "n > 0" "coprime a d"
  shows "[m = a] (mod d)" and "coprime m n"
proof (simp add: assms(2) cong_add_lcancel_0_nat cong_mult_self_right)
  have fin: "finite {p. prime p ∧ p dvd n ∧ ¬ (p dvd a)}" by (simp add: assms)
  { fix p
    assume 4: "prime p" "p dvd m" "p dvd n"
    have "p = 1"
    proof (cases "p dvd a")
      case True
      from this assms 4(2) have "p dvd q*d" 
       by (simp add: dvd_add_right_iff)
      then have a1: "p dvd q ∨ p dvd d"
       using 4(1) prime_dvd_mult_iff by blast
    
      have a2: "¬ (p dvd q)" 
      proof (rule ccontr,simp)  
       assume "p dvd q"
       then have "p dvd (∏ p | prime p ∧ p dvd n ∧ ¬ (p dvd a). p)" 
         unfolding assms by simp
       then have "∃x∈{p. prime p ∧ p dvd n ∧ ¬ p dvd a}. p dvd x"
        using prime_dvd_prod_iff[OF fin 4(1)] by simp
       then obtain x where c: "p dvd x ∧ prime x ∧ ¬ x dvd a" by blast
       then have "p = x" using 4(1) by (simp add: primes_dvd_imp_eq)
       then show "False" using True c by auto
      qed
      have a3: "¬ (p dvd d)" 
        using True assms "4"(1) coprime_def not_prime_unit by auto
  
      from a1 a2 a3 show ?thesis by simp
    next
      case False
      then have "p dvd q" 
      proof -
       have in_s: "p ∈ {p. prime p ∧ p dvd n ∧ ¬ p dvd a}"
        using False 4(3) 4(1) by simp
       show "p dvd q" 
        unfolding assms using dvd_prodI[OF fin in_s ] by fast
      qed
      then have "p dvd q*d" by simp
      then have "p dvd a" using 4(2) assms
        by (simp add: dvd_add_left_iff)
      then show ?thesis using False by auto
    qed
  }
  note lem = this
  show "coprime m n" 
  proof (subst coprime_iff_gcd_eq_1)
    {fix a 
     assume "a dvd m" "a dvd n" "a ≠ 1"
     {fix p
      assume "prime p" "p dvd a"
      then have "p dvd m" "p dvd n" 
       using ‹a dvd m› ‹a dvd n› by auto
      from lem have "p = a" 
       using not_prime_1 ‹prime p› ‹p dvd m› ‹p dvd n› by blast}
      then have "prime a" 
       using prime_prime_factor[of a] ‹a ≠ 1› by blast
      then have "a = 1" using lem ‹a dvd m› ‹a dvd n› by blast
      then have "False" using ‹a = 1› ‹a ≠ 1› by blast
    }
    then show "gcd m n = 1" by blast
  qed
qed

text ‹Theorem 8.17›
text‹The case ‹d = 1› is exactly the case described in @{thm dcharacter.one_induced_iff_principal}.›
theorem (in dcharacter) induced_modulus_altdef2:
  assumes "d dvd n" "d ≠ 1" 
  defines "χ₁ ≡ principal_dchar n"
  shows "induced_modulus d ⟷ (∃Φ. dcharacter d Φ ∧ (∀k. χ k = Φ k * χ₁ k))"
proof
  from n have n_pos: "n > 0" by simp
  assume as_im: "induced_modulus d" 
  define f where
    "f ≡ (λk. k +
      (if k = 1 then
         0
       else (prod id {p. prime p ∧ p dvd n ∧ ¬ (p dvd k)})*d)
      )"
  have [simp]: "f (Suc 0) = 1" unfolding f_def by simp
  {
    fix k
    assume as: "coprime k d" 
    hence "[f k = k] (mod d)" "coprime (f k) n" 
      using induced_modulus_altdef2_lemma[OF n_pos as] by (simp_all add: f_def)
  }
  note m_prop = this
  
  define Φ where
   "Φ ≡ (λn. (if ¬ coprime n d then 0 else χ(f n)))"

  have Φ_1: "Φ 1 = 1" 
    unfolding Φ_def by simp

  from assms(1,2) n have "d > 0" by (intro Nat.gr0I) auto
  from induced_modulus_altdef1 assms(1) ‹d > 0› as_im 
    have b: "(∀a b. coprime a n ∧ coprime b n ∧
                 [a = b] (mod d) ⟶ χ a = χ b)" by blast

  have Φ_periodic:  " ∀a. Φ (a + d) = Φ a" 
  proof 
    fix a
    have "gcd (a+d) d = gcd a d" by auto
    then have cop: "coprime (a+d) d = coprime a d"  
      using coprime_iff_gcd_eq_1 by presburger
    show "Φ (a + d) = Φ a"
    proof (cases "coprime a d")
      case True
      from True cop have cop_ad: "coprime (a+d) d" by blast      
      have p1: "[f (a+d) = f a] (mod d)" 
        using m_prop(1)[of "a+d", OF cop_ad] 
              m_prop(1)[of "a",OF True] by (simp add: unique_euclidean_semiring_class.cong_def)
      have p2: "coprime (f (a+d)) n" "coprime (f a) n" 
        using m_prop(2)[of "a+d", OF cop_ad]
              m_prop(2)[of "a", OF True] by blast+ 
      from b p1 p2 have eq: "χ (f (a + d)) = χ (f a)" by blast
      show ?thesis 
        unfolding Φ_def 
        by (subst cop,simp,safe, simp add: eq) 
    next
      case False
      then show ?thesis unfolding Φ_def by (subst cop,simp)
    qed  
  qed

  have Φ_mult: "∀a b. a ∈ totatives d ⟶
          b ∈ totatives d ⟶ Φ (a * b) = Φ a * Φ b"
  proof (safe)
    fix a b
    assume "a ∈ totatives d" "b ∈ totatives d"  
    consider (ab) "coprime a d ∧ coprime b d" | 
             (a)  "coprime a d ∧ ¬ coprime b d" |
             (b)  "coprime b d ∧ ¬ coprime a d" |
             (n)  "¬ coprime a d ∧ ¬ coprime b d" by blast
    then show "Φ (a * b) = Φ a * Φ b" 
    proof cases
      case ab 
      then have c_ab: 
        "coprime (a*b) d" "coprime a d" "coprime b d" by simp+ 
      then have p1: "[f (a * b) = a * b] (mod d)" "coprime (f (a * b)) n"
        using m_prop[of "a*b", OF c_ab(1)] by simp+
      moreover have p2: "[f a = a] (mod d)" "coprime (f a) n"
                    "[f b = b] (mod d)" "coprime (f b) n"
        using m_prop[of "a",OF c_ab(2)]
              m_prop[of "b",OF c_ab(3) ] by simp+
      have p1s: "[f (a * b) = (f a) * (f b)] (mod d)"
      proof -
        have "[f (a * b) = a * b] (mod d)"
          using p1(1) by blast
        moreover have "[a * b = f(a) * f(b)] (mod d)" 
          using p2(1) p2(3) by (simp add: cong_mult cong_sym)
        ultimately show ?thesis using cong_trans by blast
      qed
      have p2s: "coprime (f a*f b) n"
        using p2(2) p2(4) by simp
      have "χ (f (a * b)) = χ (f a * f b)" 
        using p1s p2s p1(2) b by blast 
      then show ?thesis 
        unfolding Φ_def by (simp add: c_ab)
    qed (simp_all add: Φ_def)
  qed
  have d_gr_1: "d > 1" using assms(1,2) 
    using ‹0 < d› by linarith
  show "∃Φ. dcharacter d Φ ∧ (∀n. χ n = Φ n * χ₁ n)" 
  proof (standard,rule conjI) 
    show "dcharacter d Φ" 
      unfolding dcharacter_def residues_nat_def dcharacter_axioms_def 
      using d_gr_1 Φ_def f_def Φ_mult Φ_1 Φ_periodic by simp
    show "∀n. χ n = Φ n * χ₁ n" 
    proof
      fix k
      show "χ k = Φ k * χ₁ k"
      proof (cases "coprime k n")
        case True
        then have "coprime k d" using assms(1) by auto
        then have "Φ(k) = χ(f k)" using Φ_def by simp
        moreover have "[f k = k] (mod d)" 
          using m_prop[OF ‹coprime k d›] by simp
        moreover have "χ₁ k = 1" 
          using assms(3) principal_dchar_def ‹coprime k n› by auto
        ultimately show "χ(k) = Φ(k) * χ₁(k)" 
        proof -
          assume "Φ k = χ (f k)" "[f k = k] (mod d)" "χ₁ k = 1"
          then have "χ k = χ (f k)"
            using ‹local.induced_modulus d› induced_modulus_altdef1 assms(1) ‹d > 0›
                  True ‹coprime k d› m_prop(2) by auto
          also have "… = Φ k" by (simp add: ‹Φ k = χ (f k)›)
          also have "… = Φ k * χ₁ k" by (simp add: ‹χ₁ k = 1›)
          finally show ?thesis by simp
        qed
      next
        case False
        hence "χ k = 0"
          using eq_zero_iff by blast 
        moreover have "χ₁ k = 0"
          using False assms(3) principal_dchar_def by simp       
        ultimately show ?thesis by simp
      qed      
    qed
  qed
next
  assume "(∃Φ. dcharacter d Φ ∧ (∀k. χ k = Φ k * χ₁ k))"
  then obtain Φ where 1: "dcharacter d Φ" "(∀k. χ k = Φ k * χ₁ k)" by blast
  show "induced_modulus d"
    unfolding induced_modulus_def    
  proof (rule conjI,fact,safe)
    fix k
    assume 2: "coprime k n" "[k = 1] (mod d)"
    then have "χ₁ k = 1"
      by (simp add: χ₁_def)
    moreover have "Φ k = 1"
      by (metis "1"(1) "2"(2) One_nat_def dcharacter.Suc_0 dcharacter.cong) 
    ultimately show "χ k = 1" using 1(2) by simp    
  qed
qed


subsection ‹The conductor of a character›

context dcharacter
begin

definition "conductor = Min {d. induced_modulus d}"

lemma conductor_fin: "finite {d. induced_modulus d}"
proof -
  let ?A = "{d. induced_modulus d}" 
  have "?A ⊆ {d. d dvd n}" 
    unfolding induced_modulus_def by blast
  moreover have "finite {d. d dvd n}" using n by simp
  ultimately show "finite ?A" using finite_subset by auto
qed

lemma conductor_induced: "induced_modulus conductor"
proof -
  have "{d. induced_modulus d} ≠ {}" using induced_modulus_modulus by blast
  then show "induced_modulus conductor"             
    using Min_in[OF conductor_fin ] conductor_def by auto
qed

lemma conductor_le_iff: "conductor ≤ a ⟷ (∃d≤a. induced_modulus d)"
  unfolding conductor_def using conductor_fin induced_modulus_modulus by (subst Min_le_iff) auto

lemma conductor_ge_iff: "conductor ≥ a ⟷ (∀d. induced_modulus d ⟶ d ≥ a)"
  unfolding conductor_def using conductor_fin induced_modulus_modulus by (subst Min_ge_iff) auto

lemma conductor_leI: "induced_modulus d ==> conductor ≤ d"
  by (subst conductor_le_iff) auto

lemma conductor_geI: "(∧d. induced_modulus d ==> d ≥ a) ==> conductor ≥ a"
  by (subst conductor_ge_iff) auto

lemma conductor_dvd: "conductor dvd n"
  using conductor_induced unfolding induced_modulus_def by blast

lemma conductor_le_modulus: "conductor ≤ n"
  using conductor_dvd by (rule dvd_imp_le) (use n in auto)

lemma conductor_gr_0: "conductor > 0"
  unfolding conductor_def using zero_not_ind_mod 
  using conductor_def conductor_induced neq0_conv by fastforce

lemma conductor_eq_1_iff_principal: "conductor = 1 ⟷ χ = principal_dchar n" 
proof
  assume "conductor = 1" 
  then have "induced_modulus 1"
    using conductor_induced by auto
  then show "χ = principal_dchar n"
    using one_induced_iff_principal by blast
next
  assume "χ = principal_dchar n"
  then have im_1: "induced_modulus 1" using one_induced_iff_principal by auto
  show "conductor = 1" 
  proof -
    have "conductor ≤ 1" 
      using conductor_fin Min_le[OF conductor_fin,simplified,OF im_1]
      by (simp add: conductor_def[symmetric])
    then show ?thesis using conductor_gr_0 by auto
  qed
qed

lemma conductor_principal [simp]: "χ = principal_dchar n ==> conductor = 1"
  by (subst conductor_eq_1_iff_principal)
  
lemma nonprimitive_imp_conductor_less:
  assumes "¬primitive_dchar n χ"
  shows "conductor < n" 
proof -
  obtain d where d: "induced_modulus d" "d < n" 
    using primitive_dchar_iff assms by blast
  from d(1) have "conductor ≤ d"
    by (rule conductor_leI)
  also have "… < n" by fact
  finally show ?thesis .
qed

lemma (in nonprimitive_dchar) conductor_less_modulus: "conductor < n"
  using nonprimitive_imp_conductor_less nonprimitive by metis


text ‹Theorem 8.18›
theorem primitive_principal_form:
  defines "χ₁ ≡ principal_dchar n"
  assumes "χ ≠ principal_dchar n"
  shows "∃Φ. primitive_dchar conductor Φ ∧ (∀n. χ(n) = Φ(n) * χ₁(n))"
proof -
  (*
    TODO: perhaps residues_nat should be relaxed to allow n = 1.
    Then we could remove the unnecessary precondition here.
    It makes no real difference though.
  *)
  from n have n_pos: "n > 0" by simp
  define d where "d = conductor" 
  have induced: "induced_modulus d" 
    unfolding d_def using conductor_induced by blast
  then have d_not_1: "d ≠ 1" 
    using one_induced_iff_principal assms by auto
  hence d_gt_1: "d > 1" using conductor_gr_0 by (auto simp: d_def)
  
  from induced obtain Φ where Φ_def: "dcharacter d Φ ∧ (∀n. χ n = Φ n * χ₁ n)"
    using d_not_1
    by (subst (asm) induced_modulus_altdef2) (auto simp: d_def conductor_dvd χ₁_def)
  have phi_dchars: "Φ ∈ dcharacters d" using Φ_def dcharacters_def by auto

  interpret Φ: dcharacter d "residue_mult_group d" Φ
    using Φ_def by auto

  have Φ_prim: "primitive_dchar d Φ" 
  proof (rule ccontr)
    assume "¬ primitive_dchar d Φ"   
    then obtain q where 
      1: "q dvd d ∧ q < d ∧ Φ.induced_modulus q"
      unfolding Φ.induced_modulus_def Φ.primitive_dchar_iff by blast
    then have 2: "induced_modulus q" 
    proof -
      {fix k
      assume mod_1: "[k = 1] (mod q)" 
      assume cop: "coprime k n" 
      have "χ(k) = Φ(k)*χ₁(k)" using Φ_def by auto
      also have "… = Φ(k)" 
        using cop by (simp add: assms principal_dchar_def)  
      also have "… = 1" 
          using 1 mod_1 Φ.induced_modulus_def 
                ‹induced_modulus d› cop induced_modulus_def by auto
      finally have "χ(k) = 1" by blast}

      then show ?thesis 
        using induced_modulus_def "1" ‹induced_modulus d› by auto
    qed
     
    from 1 have "q < d" by simp
    moreover have "d ≤ q" unfolding d_def
      by (intro conductor_leI) fact
    ultimately show False by linarith
  qed     

  from Φ_def Φ_prim d_def phi_dchars show ?thesis by blast
qed

definition primitive_extension :: "nat ==> complex" where
  "primitive_extension =
     (SOME Φ. primitive_dchar conductor Φ ∧ (∀k. χ k = Φ k * principal_dchar n k))"

lemma
  assumes nonprincipal: "χ ≠ principal_dchar n"
  shows primitive_primitive_extension: "primitive_dchar conductor primitive_extension"
    and principal_decomposition:       "χ k = primitive_extension k * principal_dchar n k"
proof -
  note * = someI_ex[OF primitive_principal_form[OF nonprincipal], folded primitive_extension_def]
  from * show "primitive_dchar conductor primitive_extension" by blast
  from * show "χ k = primitive_extension k * principal_dchar n k" by blast
qed

end


subsection ‹The connection between primitivity and separability›

lemma residue_mult_group_coset:
  fixes m n m1 m2 :: nat and f :: "nat ==> nat" and G H
  defines "G ≡ residue_mult_group n"
  defines "H ≡ residue_mult_group m"
  defines "f ≡ (λk. k mod m)"
  assumes "b ∈ (rcosets kernel G H f)"
  assumes "m1 ∈ b" "m2 ∈ b"
  assumes "n > 1" "m dvd n"
  shows "m1 mod m = m2 mod m"
proof -
  have h_1: "1 = 1" 
    using assms(2) unfolding residue_mult_group_def totatives_def by simp
    
  from assms(4)
  obtain a :: nat where cos_expr: "b = (kernel G H f) #> a ∧ a ∈ carrier G" 
    using RCOSETS_def[of G "kernel G H f"] by blast
  then have cop: "coprime a n" 
    using assms(1) unfolding residue_mult_group_def totatives_def by auto
  
  obtain a' where "[a * a' = 1] (mod n)"
    using cong_solve_coprime_nat[OF cop] by auto
  then have a_inv: "(a*a') mod n = 1" 
    using unique_euclidean_semiring_class.cong_def[of "a*a'" 1 n] assms(7) by simp

  have "m1 ∈ (∪h∈kernel G H f. {h ⊗ a})"
       "m2 ∈ (∪h∈kernel G H f. {h ⊗ a})"
    using r_coset_def[of G "kernel G H f" a] cos_expr assms(5,6) by blast+
  then have "m1 ∈ (∪h∈kernel G H f. {(h * a) mod n})"
            "m2 ∈ (∪h∈kernel G H f. {(h * a) mod n})"
    using assms(1) unfolding residue_mult_group_def[of n] by auto
  then obtain m1' m2' where 
    m_expr: "m1 = (m1'* a) mod n ∧ m1' ∈ kernel G H f" 
            "m2 = (m2'* a) mod n ∧ m2' ∈ kernel G H f" 
    by blast

  have eq_1: "m1 mod m = a mod m" 
  proof -
    have "m1 mod m = ((m1'* a) mod n) mod m" using m_expr by blast
    also have "… = (m1' * a) mod m" 
      using euclidean_semiring_cancel_class.mod_mod_cancel assms(8) by blast
    also have "… = (m1' mod m) * (a mod m) mod m" 
      by (simp add: mod_mult_eq)
    also have "… = (a mod m) mod m" 
      using m_expr(1) h_1 unfolding kernel_def assms(3) by simp
    also have "… = a mod m" by auto
    finally show ?thesis by simp
  qed

  have eq_2: "m2 mod m = a mod m" 
  proof -
    have "m2 mod m = ((m2'* a) mod n) mod m" using m_expr by blast
    also have "… = (m2' * a) mod m" 
      using euclidean_semiring_cancel_class.mod_mod_cancel assms(8) by blast
    also have "… = (m2' mod m) * (a mod m) mod m" 
      by (simp add: mod_mult_eq)
    also have "… = (a mod m) mod m" 
      using m_expr(2) h_1 unfolding kernel_def assms(3) by simp
    also have "… = a mod m" by auto
    finally show ?thesis by simp
  qed

  from eq_1 eq_2 show ?thesis by argo
qed

lemma residue_mult_group_kernel_partition:
  fixes m n :: nat and f :: "nat ==> nat" and G H
  defines "G ≡ residue_mult_group n"
  defines "H ≡ residue_mult_group m"
  defines "f ≡ (λk. k mod m)"
  assumes "m > 1" "n > 0" "m dvd n" 
  shows "partition (carrier G) (rcosets kernel G H f)"
        and "card (rcosets kernel G H f) = totient m"
        and "card (kernel G H f) = totient n div totient m"
        and "b ∈(rcosets kernel G H f) ==> b ≠ {}"
        and "b ∈(rcosets kernel G H f) ==> card (kernel G H f) = card b"
        and "bij_betw (λb. (the_elem (f ` b))) (rcosets kernel G H f) (carrier H)"
proof -
  have "1 < m" by fact
  also have "m ≤ n" using ‹n > 0› ‹m dvd n› by (intro dvd_imp_le) auto
  finally have "n > 1" .
  note mn = ‹m > 1› ‹n > 1› ‹m dvd n› ‹m ≤ n›

  interpret n: residues_nat n G
    using mn by unfold_locales (auto simp: assms)
  interpret m: residues_nat m H
    using mn by unfold_locales (auto simp: assms)
  
  from mn have subset: "f ` carrier G ⊆ carrier H"
    by (auto simp: assms(1-3) residue_mult_group_def totatives_def
             dest: coprime_common_divisor_nat intro!: Nat.gr0I)
  moreover have super_set: "carrier H ⊆ f ` carrier G"
  proof safe
    fix k assume "k ∈ carrier H"
    hence k: "k > 0" "k ≤ m" "coprime k m"             
      by (auto simp: assms(2) residue_mult_group_def totatives_def)
    from mn ‹k ∈ carrier H› have "k < m"
      by (simp add: totatives_less assms(2) residue_mult_group_def)
    define P where "P = {p ∈ prime_factors n. ¬(p dvd m)}"
    define a where "a = ∏P"
    have [simp]: "a ≠ 0" by (auto simp: P_def a_def intro!: Nat.gr0I)
    have [simp]: "prime_factors a = P"
    proof -
      have "prime_factors a = set_mset (sum prime_factorization P)"
        unfolding a_def using mn
        by (subst prime_factorization_prod)
           (auto simp: P_def prime_factors_dvd prime_gt_0_nat)
      also have "sum prime_factorization P = (∑p∈P. {#p#})"
        using mn by (intro sum.cong) (auto simp: P_def prime_factorization_prime prime_factors_dvd)
      finally show ?thesis by (simp add: P_def)
    qed

    from mn have "coprime m a"
      by (subst coprime_iff_prime_factors_disjoint) (auto simp: P_def)
    hence "∃x. [x = k] (mod m) ∧ [x = 1] (mod a)"
      by (intro binary_chinese_remainder_nat)
    then obtain x where x: "[x = k] (mod m)" "[x = 1] (mod a)"
      by auto
    from x(1) mn k have [simp]: "x ≠ 0"
      by (meson ‹k < m› cong_0_iff cong_sym_eq nat_dvd_not_less)
      
    from x(2) have "coprime x a"
      using cong_imp_coprime cong_sym by force
    hence "coprime x (a * m)"
      using k cong_imp_coprime[OF cong_sym[OF x(1)]] by auto
    also have "?this ⟷ coprime x n" using mn
      by (intro coprime_cong_prime_factors)
         (auto simp: prime_factors_product P_def in_prime_factors_iff)
    finally have "x mod n ∈ totatives n"
      using mn by (auto simp: totatives_def intro!: Nat.gr0I)

    moreover have "f (x mod n) = k"
      using x(1) k mn ‹k < m› by (auto simp: assms(3) unique_euclidean_semiring_class.cong_def mod_mod_cancel)
    ultimately show "k ∈ f ` carrier G"
      by (auto simp: assms(1) residue_mult_group_def)
  qed

  ultimately have image_eq: "f ` carrier G = carrier H" by blast

  have [simp]: "f (k ⊗ l) = f k ⊗ f l" if "k ∈ carrier G" "l ∈ carrier G" for k l
    using that mn by (auto simp: assms(1-3) residue_mult_group_def totatives_def
                                 mod_mod_cancel mod_mult_eq)
  interpret f: group_hom G H f
    using subset by unfold_locales (auto simp: hom_def)

  show "bij_betw (λb. (the_elem (f ` b))) (rcosets kernel G H f) (carrier H)"
    unfolding bij_betw_def  
  proof 
    show "inj_on (λb. (the_elem (f ` b))) (rcosets kernel G H f)"
      using f.FactGroup_inj_on unfolding FactGroup_def by auto
    have eq: "f ` carrier G = carrier H" 
      using subset super_set by blast
    show "(λb. the_elem (f ` b)) ` (rcosets kernel G H f) = carrier H"
      using f.FactGroup_onto[OF eq] unfolding FactGroup_def by simp
  qed
  
  show "partition (carrier G) (rcosets kernel G H f)"
  proof 
    show "∧a. a ∈ carrier G ==>
         ∃!b. b ∈ rcosets kernel G H f ∧ a ∈ b"
    proof -
      fix a
      assume a_in: "a ∈ carrier G"
      show "∃!b. b ∈ rcosets kernel G H f ∧ a ∈ b"
      proof -
       (*exists*)
        have "∃b. b ∈ rcosets kernel G H f ∧ a ∈ b"
          using a_in n.rcosets_part_G[OF f.subgroup_kernel]
          by blast
        then show ?thesis
          using group.rcos_disjoint[OF n.is_group f.subgroup_kernel]
          by (auto simp: disjoint_def)
      qed       
    qed
  next
    show "∧b. b ∈ rcosets kernel G H f ==> b ⊆ carrier G"
      using n.rcosets_part_G f.subgroup_kernel by auto
  qed
   
  (* sizes *)
  have lagr: "card (carrier G) = card (rcosets kernel G H f) * card (kernel G H f)" 
        using group.lagrange_finite[OF n.is_group n.fin f.subgroup_kernel] Coset.order_def[of G] by argo
  have k_size: "card (kernel G H f) > 0" 
    using f.subgroup_kernel finite_subset n.subgroupE(1) n.subgroupE(2) by fastforce
  have G_size: "card (carrier G) = totient n"
    using n.order Coset.order_def[of G] by simp
  have H_size: " totient m = card (carrier H)"
    using n.order Coset.order_def[of H] by simp
  also have "… = card (carrier (G Mod kernel G H f))" 
    using f.FactGroup_iso[OF image_eq] card_image f.FactGroup_inj_on f.FactGroup_onto image_eq by fastforce
  also have "… = card (carrier G) div card (kernel G H f)"
  proof -    
    have "card (carrier (G Mod kernel G H f)) =
          card (rcosets kernel G H f)" 
      unfolding FactGroup_def by simp
    also have "… = card (carrier G) div card (kernel G H f)"
      by (simp add: lagr k_size)
    finally show ?thesis by blast
  qed
  also have "… = totient n div card (kernel G H f)"
    using G_size by argo
  finally have eq: "totient m = totient n div card (kernel G H f)" by simp
  show "card (kernel G H f) = totient n div totient m"
  proof -
    have "totient m ≠ 0" 
      using totient_0_iff[of m] assms(4) by blast
    have "card (kernel G H f) dvd totient n" 
      using lagr ‹card (carrier G) = totient n› by auto
    have "totient m * card (kernel G H f) = totient n"
      unfolding eq using ‹card (kernel G H f) dvd totient n› by auto
    have "totient n div totient m = totient m * card (kernel G H f) div totient m"
      using ‹totient m * card (kernel G H f) = totient n› by auto
    also have "… = card (kernel G H f)"
      using nonzero_mult_div_cancel_left[OF ‹totient m ≠ 0›] by blast
    finally show ?thesis by auto
  qed

  show "card (rcosets kernel G H f) = totient m"
  proof -
    have H_size: " totient m = card (carrier H)"
      using n.order Coset.order_def[of H] by simp
    also have "… = card (carrier (G Mod kernel G H f))" 
      using f.FactGroup_iso[OF image_eq] card_image f.FactGroup_inj_on f.FactGroup_onto image_eq by fastforce
    also have "card (carrier (G Mod kernel G H f)) =
          card (rcosets kernel G H f)" 
      unfolding FactGroup_def by simp 
    finally show "card (rcosets kernel G H f) = totient m"
      by argo
  qed

  assume "b ∈ rcosets kernel G H f"
  then show "b ≠ {}"
  proof -
    have "card b = card (kernel G H f)"
      using ‹b ∈ rcosets kernel G H f› f.subgroup_kernel n.card_rcosets_equal n.subgroupE(1) by auto
    then have "card b > 0" 
      by (simp add: k_size)
    then show ?thesis by auto
  qed

  assume b_cos: "b ∈ rcosets kernel G H f"
  show "card (kernel G H f) = card b" 
    using group.card_rcosets_equal[OF n.is_group b_cos] 
          f.subgroup_kernel subgroup.subset by blast    
qed


lemma primitive_iff_separable_lemma:
 assumes prod: "(∀n. χ n = Φ n * χ₁ n) ∧ primitive_dchar d Φ"
 assumes ‹d > 1› ‹0 < k› ‹d dvd k› ‹k > 1›
 shows "(∑m | m ∈ {1..k} ∧ coprime m k. Φ(m) * unity_root d m) =
        (totient k div totient d) * (∑m | m ∈ {1..d} ∧ coprime m d. Φ(m) * unity_root d m)"
proof -
  from assms interpret Φ: primitive_dchar d "residue_mult_group d" Φ
    by auto
  define G where "G = residue_mult_group k"
  define H where "H = residue_mult_group d"
  define f where "f = (λt. t mod d)" 
  
  from residue_mult_group_kernel_partition(2)[OF ‹d > 1› ‹0 < k› ‹d dvd k›]
  have fin_cosets: "finite (rcosets kernel G H f)"         
   using ‹1 < d› card.infinite by (fastforce simp: G_def H_def f_def)
          
  have fin_G: "finite (carrier G)"
    unfolding G_def residue_mult_group_def by simp
  
  have eq: "(∑m | m ∈ {1..k} ∧ coprime m k. Φ(m) * unity_root d m) =
         (∑m | m ∈ carrier G . Φ(m) * unity_root d m)"
   unfolding residue_mult_group_def totatives_def G_def
   by (rule sum.cong,auto)
  also have "… = sum (λm. Φ(m) * unity_root d m) (carrier G)" by simp
  also have eq': "… = sum (sum (λm. Φ m * unity_root d (int m))) (rcosets kernel G H f)"
    by (rule disjoint_sum [symmetric])
       (use fin_G fin_cosets residue_mult_group_kernel_partition(1)[OF ‹d > 1› ‹k > 0› ‹d dvd k›] in
          ‹auto simp: G_def H_def f_def›)
  also have "… =
   (∑b ∈ (rcosets kernel G H f) . (∑m ∈ b. Φ m * unity_root d (int m)))" by simp
  finally have 1: "(∑m | m ∈ {1..k} ∧ coprime m k. Φ(m) * unity_root d m) =
                   (∑b ∈ (rcosets kernel G H f) . (∑m ∈ b. Φ m * unity_root d (int m)))" 
    using eq eq' by auto
  have eq''': "… =
    (∑b ∈ (rcosets kernel G H f) . (totient k div totient d) * (Φ (the_elem (f ` b)) * unity_root d (int (the_elem (f ` b)))))"
  proof (rule sum.cong,simp) 
    fix b
    assume b_in: "b ∈ (rcosets kernel G H f)" 
    note b_not_empty = residue_mult_group_kernel_partition(4)
                         [OF ‹d > 1› ‹0 < k› ‹d dvd k› b_in[unfolded G_def H_def f_def]] 
  
    {
      fix m1 m2
      assume m_in: "m1 ∈ b" "m2 ∈ b" 
      have m_mod: "m1 mod d = m2 mod d"   
        using residue_mult_group_coset[OF b_in[unfolded G_def H_def f_def] m_in ‹k > 1› ‹d dvd k›]
        by blast
    } note m_mod = this
    {
      fix m1 m2
      assume m_in: "m1 ∈ b" "m2 ∈ b" 
      have "Φ m1 * unity_root d (int m1) = Φ m2 * unity_root d (int m2)"
      proof -
        have Φ_periodic: "periodic_arithmetic Φ d" using Φ.dir_periodic_arithmetic by blast
        have 1: "Φ m1 = Φ m2" 
         using mod_periodic_arithmetic[OF ‹periodic_arithmetic Φ d› m_mod[OF m_in]] by simp 
       have 2: "unity_root d m1 = unity_root d m2"
         using m_mod[OF m_in] by (intro unity_root_cong) (auto simp: unique_euclidean_semiring_class.cong_def simp flip: zmod_int)
       from 1 2 show ?thesis by simp
      qed
    } note all_eq_in_coset = this   
   
    from all_eq_in_coset b_not_empty 
    obtain l where l_prop: "l ∈ b ∧ (∀y ∈ b. Φ y * unity_root d (int y) =
                                Φ l * unity_root d (int l))" by blast
     
    have "(∑m ∈ b. Φ m * unity_root d (int m)) =
            ((totient k div totient d) * (Φ l * unity_root d (int l)))"
    proof -
      have "(∑m ∈ b. Φ m * unity_root d (int m)) =
              (∑m ∈ b. Φ l * unity_root d (int l))"              
          by (rule sum.cong,simp) (use all_eq_in_coset l_prop in blast)
      also have "… = card b * Φ l * unity_root d (int l)"
        by simp
      also have "… = (totient k div totient d) * Φ l * unity_root d (int l)"
        using residue_mult_group_kernel_partition(3)[OF ‹d > 1› ‹0 < k› ‹d dvd k›] 
              residue_mult_group_kernel_partition(5)
                [OF ‹d > 1› ‹0 < k› ‹d dvd k› b_in [unfolded G_def H_def f_def]]
        by argo
      finally have 2:
        "(∑m ∈ b. Φ m * unity_root d (int m)) =
         (totient k div totient d) * Φ l * unity_root d (int l)" 
        by blast
      from b_not_empty 2 show ?thesis by auto
    qed
    also have "… = ((totient k div totient d) * (Φ (the_elem (f ` b)) * unity_root d (int (the_elem (f ` b)))))"
    proof -
      have foral: "(∧y. y ∈ b ==> f y = f l)" 
         using m_mod l_prop unfolding f_def by blast
      have eq: "the_elem (f ` b) = f l"
        by (simp add: b_not_empty foral the_elem_image_unique)
      have per: "periodic_arithmetic Φ d" using prod Φ.dir_periodic_arithmetic by blast
      show ?thesis
        unfolding eq using mod_periodic_arithmetic[OF per, of "l mod d" l]
        by (auto simp: f_def unity_root_mod zmod_int)
    qed
  finally show "(∑m ∈ b. Φ m * unity_root d (int m)) =
                 ((totient k div totient d) * (Φ (the_elem (f ` b)) * unity_root d (int (the_elem (f ` b)))))"
    by blast
  qed
  have "… =
             (∑b ∈ (rcosets kernel G H f) . (totient k div totient d) * (Φ (the_elem (f ` b)) * unity_root d (int (the_elem (f ` b)))))"
    by blast
  also have eq'': "
     … = (∑h ∈ carrier H . (totient k div totient d) * (Φ (h) * unity_root d (int (h))))"
    unfolding H_def G_def f_def
    by (rule sum.reindex_bij_betw[OF residue_mult_group_kernel_partition(6)[OF ‹d > 1› ‹0 < k› ‹d dvd k›]])
  finally have 2: "(∑m | m ∈ {1..k} ∧ coprime m k. Φ(m) * unity_root d m) =
                  (totient k div totient d)*(∑h ∈ carrier H . (Φ (h) * unity_root d (int (h))))"
    using 1 by (simp add: eq'' eq''' sum_distrib_left)
  also have "… = (totient k div totient d)*(∑m | m ∈ {1..d} ∧ coprime m d . (Φ (m) * unity_root d (int (m))))"
    unfolding H_def residue_mult_group_def by (simp add: totatives_def Suc_le_eq)
  finally show ?thesis by simp
qed


text ‹Theorem 8.19›
theorem (in dcharacter) primitive_iff_separable:
  "primitive_dchar n χ ⟷ (∀k>0. separable k)"
proof (cases "χ = principal_dchar n")
  case True
  thus ?thesis
    using principal_not_primitive principal_not_totally_separable by auto
next
  case False
  note nonprincipal = this
  show ?thesis
  proof 
    assume "primitive_dchar n χ" 
    then interpret A: primitive_dchar n "residue_mult_group n" χ by auto
    show "(∀k. k > 0 ⟶ separable k)" 
      using n A.primitive_encoding(2) by blast
  next
    assume tot_separable: "∀k>0. separable k" 
    {
      assume as: "¬ primitive_dchar n χ"
      have "∃r. r ≠ 0 ∧ ¬ coprime r n ∧ gauss_sum r ≠ 0"
      proof -
        from n have "n > 0" by simp
        define d where "d = conductor"
        have "d > 0" unfolding d_def using conductor_gr_0 .
        then have "d > 1" using nonprincipal d_def conductor_eq_1_iff_principal by auto
        have "d < n" unfolding d_def using nonprimitive_imp_conductor_less[OF as] .
        have "d dvd n" unfolding d_def using conductor_dvd by blast
        define r where "r = n div d"
        have 0: "r ≠ 0" unfolding r_def 
          using ‹0 < n› ‹d dvd n› dvd_div_gt0 by auto
        have "gcd r n > 1" 
          unfolding r_def 
        proof -  
          have "n div d > 1" using ‹1 < n› ‹d < n› ‹d dvd n› by auto
          have "n div d dvd n" using ‹d dvd n› by force 
          have "gcd (n div d) n = n div d" using gcd_nat.absorb1[OF ‹n div d dvd n›] by blast
          then show "1 < gcd (n div d) n" using ‹n div d > 1› by argo
        qed
        then have 1: "¬ coprime r n" by auto
        define χ₁ where "χ₁ = principal_dchar n"
        from primitive_principal_form[OF nonprincipal]
        obtain Φ where 
           prod: "(∀k. χ(k) = Φ(k)*χ₁(k)) ∧ primitive_dchar d Φ" 
          using d_def unfolding χ₁_def by blast
        then have prod1: "(∀k. χ(k) = Φ(k)*χ₁(k))" "primitive_dchar d Φ" by blast+ 
        then interpret Φ: primitive_dchar d "residue_mult_group d" Φ
          by auto
    
        have "gauss_sum r = (∑m = 1..n . χ(m) * unity_root n (m*r))"
          unfolding gauss_sum_def by blast
        also have "… = (∑m = 1..n . Φ(m)*χ₁(m) * unity_root n (m*r))"
          by (rule sum.cong,auto simp add: prod) 
        also have "… = (∑m | m ∈ {1..n} ∧ coprime m n. Φ(m)*χ₁(m) * unity_root n (m*r))"
          by (intro sum.mono_neutral_right) (auto simp: χ₁_def principal_dchar_def)
        also have "… = (∑m | m ∈ {1..n} ∧ coprime m n. Φ(m)*χ₁(m) * unity_root d m)"
        proof (rule sum.cong,simp)
          fix x
          assume "x ∈ {m ∈ {1..n}. coprime m n}" 
          have "unity_root n (int (x * r)) = unity_root d (int x)"
            using unity_div_num[OF ‹n > 0› ‹d > 0› ‹d dvd n›]
            by (simp add: algebra_simps r_def)
          then show "Φ x * χ₁ x * unity_root n (int (x * r)) =
                     Φ x * χ₁ x * unity_root d (int x)" by auto
        qed
        also have "… = (∑m | m ∈ {1..n} ∧ coprime m n. Φ(m) * unity_root d m)"
          by (rule sum.cong,auto simp add: χ₁_def principal_dchar_def)
        also have "… = (totient n div totient d) * (∑m | m ∈ {1..d} ∧ coprime m d. Φ(m) * unity_root d m)"
          using primitive_iff_separable_lemma[OF prod ‹d > 1› ‹n > 0› ‹d dvd n› ‹n > 1›] by blast
        also have "… = (totient n div totient d) * Φ.gauss_sum 1"
        proof -
          have "Φ.gauss_sum 1 = (∑m = 1..d . Φ m * unity_root d (int (m )))"
            by (simp add: Φ.gauss_sum_def)
          also have "… = (∑m | m ∈ {1..d} . Φ m * unity_root d (int m))"
            by (rule sum.cong,auto)
          also have "… = (∑m | m ∈ {1..d} ∧ coprime m d. Φ(m) * unity_root d m)"
            by (rule sum.mono_neutral_right) (use Φ.eq_zero in auto)
          finally have "Φ.gauss_sum 1 = (∑m | m ∈ {1..d} ∧ coprime m d. Φ(m) * unity_root d m)"
            by blast
          then show ?thesis by metis
        qed
        finally have g_expr: "gauss_sum r = (totient n div totient d) * Φ.gauss_sum 1"
          by blast
        have t_non_0: "totient n div totient d ≠ 0"
          by (simp add: ‹0 < n› ‹d dvd n› dvd_div_gt0 totient_dvd) 
        have "(norm (Φ.gauss_sum 1))² = d" 
          using Φ.primitive_encoding(3) by simp  
        then have "Φ.gauss_sum 1 ≠ 0" 
          using ‹0 < d› by auto
        then have 2: "gauss_sum r ≠ 0"
          using g_expr t_non_0 by auto
        from 0 1 2 show "∃r. r ≠ 0 ∧ ¬ coprime r n ∧ gauss_sum r ≠ 0" 
          by blast
      qed
    }
    note contr = this
   
    show "primitive_dchar n χ"
    proof (rule ccontr)
      assume "¬ primitive_dchar n χ"
      then obtain r where 1: "r ≠ 0 ∧ ¬ coprime r n ∧ gauss_sum r ≠ 0"
        using contr by blast
      from global_separability_condition tot_separable 
      have 2: "(∀k>0. ¬ coprime k n ⟶ gauss_sum k = 0)" 
        by blast
      from 1 2 show "False" by blast
    qed
  qed
qed


text‹Theorem 8.20›
theorem (in primitive_dchar) fourier_primitive:
  includes no vec_lambda_syntax
  fixes τ :: complex
  defines "τ ≡ gauss_sum 1 / sqrt n"
  shows   "χ m = τ / sqrt n * (∑k=1..n. cnj (χ k) * unity_root n (-m*k))"
  and     "norm τ = 1"
proof -
  have chi_not_principal: "χ ≠ principal_dchar n" 
    using principal_not_totally_separable primitive_encoding(2) by blast

  then have case_0: "(∑k=1..n. χ k) = 0"
  proof -
    have "sum χ {0..n-1} = sum χ {1..n}"
      using periodic_arithmetic_sum_periodic_arithmetic_shift[OF dir_periodic_arithmetic, of 1] n
      by auto
    also have "{0..n-1} = {..<n}"
      using n by auto
    finally show "(∑n = 1..n . χ n) = 0"
      using sum_dcharacter_block chi_not_principal by simp
  qed

  have "χ m =
    (∑k = 1..n. 1 / of_nat n * gauss_sum_int (- int k) *
      unity_root n (int (m * k)))"
    using dcharacter_fourier_expansion[of m] by auto
  also have "… = (∑k = 1..n. 1 / of_nat n * gauss_sum (nat ((- k) mod n)) *
      unity_root n (int (m * k)))"
    by (auto simp: gauss_sum_int_conv_gauss_sum)
  also have "… = (∑k = 1..n. 1 / of_nat n * cnj (χ (nat ((- k) mod n))) * gauss_sum 1 * unity_root n (int (m * k)))"
  proof (rule sum.cong,simp)
    fix k
    assume "k ∈ {1..n}" 
    have "gauss_sum (nat (- int k mod int n)) =
          cnj (χ (nat (- int k mod int n))) * gauss_sum 1"
    proof (cases "nat ((- k) mod n) > 0")
      case True
      then show ?thesis 
        using mp[OF spec[OF primitive_encoding(2)] True]
        unfolding separable_def by auto
    next
      case False
      then have nat_0: "nat ((- k) mod n) = 0" by blast
      show ?thesis 
      proof -
        have "gauss_sum (nat (- int k mod int n)) = gauss_sum 0" 
          using nat_0 by argo
        also have "… = (∑m = 1..n. χ m)" 
          unfolding gauss_sum_def by (rule sum.cong) auto
        also have "… = 0" using case_0 by blast
        finally have 1: "gauss_sum (nat (- int k mod int n)) = 0"
          by blast

        have 2: "cnj (χ (nat (- int k mod int n))) = 0"
          using nat_0 zero_eq_0 by simp
        show ?thesis using 1 2 by simp
      qed
    qed
    then show "1 / of_nat n * gauss_sum (nat (- int k mod int n)) * unity_root n (int (m * k)) =
               1 / of_nat n * cnj (χ (nat (- int k mod int n))) * gauss_sum 1 * unity_root n (int (m * k))" 
      by auto
  qed
  also have "… = (∑k = 1..n. 1 / of_nat n * cnj (χ (nat (- int k mod int n))) *
                    gauss_sum 1 * unity_root n (int (m * (nat (int k mod int n)))))"
  proof (rule sum.cong,simp)
    fix x   
    assume "x ∈ {1..n}" 
    have "unity_root n (m * x) = unity_root n (m * x mod n)"
      using unity_root_mod_nat[of n "m*x"] by (simp add: nat_mod_as_int)
    also have "… = unity_root n (m * (x mod n))"
      by (metis mod_mult_right_eq nat_mod_as_int unity_root_mod_nat)
    finally have "unity_root n (m * x) = unity_root n (m * (x mod n))" by blast
    then show "1 / of_nat n * cnj (χ (nat (- int x mod int n))) *
                 gauss_sum 1 * unity_root n (int (m * x)) =
               1 / of_nat n * cnj (χ (nat (- int x mod int n))) * gauss_sum 1 *
                 unity_root n (int (m * nat (int x mod int n)))" 
      by (simp add: nat_mod_as_int)    
  qed
  also have "… = (∑k = 0..n-1. 1 / of_nat n * cnj (χ k) * gauss_sum 1 * unity_root n (- int (m * k)))"
  proof -
    have b: "bij_betw (λk. nat((-k) mod n)) {1..n} {0..n-1}"
      unfolding bij_betw_def
    proof 
      show "inj_on (λk. nat (- int k mod int n)) {1..n}"
        unfolding inj_on_def
      proof (safe)
        fix x y
        assume a1: "x ∈ {1..n}" "y ∈ {1..n}"
        assume a2: "nat (- x mod n) = nat (- y mod n)"
        then have "(- x) mod n = - y mod n"
          using n eq_nat_nat_iff by auto
        then have "[-int x = - int y] (mod n)" 
          using unique_euclidean_semiring_class.cong_def by blast
        then have "[x = y] (mod n)" 
          by (simp add: cong_int_iff cong_minus_minus_iff)
        then have cong: "x mod n = y mod n" using unique_euclidean_semiring_class.cong_def by blast
        then show "x = y"
        proof (cases "x = n")
          case True then show ?thesis using cong a1(2) by auto
        next
          case False
          then have "x mod n = x" using a1(1) by auto
          then have "y ≠ n" using a1(1) local.cong by fastforce
          then have "y mod n = y" using a1(2) by auto
          then show ?thesis using ‹x mod n = x› cong by linarith
        qed
      qed
      show "(λk. nat (- int k mod int n)) ` {1..n} = {0..n - 1}"
        unfolding image_def 
      proof
        let ?A = "{y. ∃x∈{1..n}. y = nat (- int x mod int n)}"
        let ?B = "{0..n - 1}" 
        show "?A ⊆ ?B" 
        proof
          fix y
          assume "y ∈ {y. ∃x∈{1..n}. y = nat (- int x mod int n)}"
          then obtain x where "x∈{1..n} ∧ y = nat (- int x mod int n)" by blast
          then show "y ∈ {0..n - 1}" by (simp add: nat_le_iff of_nat_diff)
        qed
        show "?A 🪙 ?B" 
        proof 
          fix x
          assume 1: "x ∈ {0..n-1}"
          then have "n - x ∈ {1..n}"
            using n by auto
          have "x = nat (- int (n-x) mod int n)"
          proof -
            have "nat (- int (n-x) mod int n) = nat (int x) mod int n"
              apply(simp add: int_ops(6),rule conjI)
              using ‹n - x ∈ {1..n}› by force+
            also have "… = x" 
              using 1 n by auto
            finally show ?thesis by presburger
          qed
          then show "x ∈ {y. ∃x∈{1..n}. y = nat (- int x mod int n)}"
            using ‹n - x ∈ {1..n}› by blast
        qed
      qed
    qed
    show ?thesis 
    proof -
      have 1: "(∑k = 1..n. 1 / of_nat n * cnj (χ (nat (- int k mod int n))) *
        gauss_sum 1 * unity_root n (int (m * nat (int k mod int n)))) =
            (∑x = 1..n. 1 / of_nat n * cnj (χ (nat (- int x mod int n))) *
        gauss_sum 1 * unity_root n (- int (m * nat (- int x mod int n))))"
      proof (rule sum.cong,simp)
        fix x        
        have "(int m * (int x mod int n)) mod n = (m*x) mod n"
          by (simp add: mod_mult_right_eq zmod_int)
        also have "… = (- ((- int (m*x) mod n))) mod n"
          by (simp add: mod_minus_eq of_nat_mod)
        have "(int m * (int x mod int n)) mod n = (- (int m * (- int x mod int n))) mod n"
          apply(subst mod_mult_right_eq,subst add.inverse_inverse[symmetric],subst (5) add.inverse_inverse[symmetric])
          by (subst minus_mult_minus,subst mod_mult_right_eq[symmetric],auto)
        then have "unity_root n (int m * (int x mod int n)) =
                   unity_root n (- (int m * (- int x mod int n)))"
          using unity_root_mod[of n "int m * (int x mod int n)"] 
                 unity_root_mod[of n " - (int m * (- int x mod int n))"] by argo
        then show "1 / of_nat n * cnj (χ (nat (- int x mod int n))) *
         gauss_sum 1 *
         unity_root n (int (m * nat (int x mod int n))) =
         1 / of_nat n * cnj (χ (nat (- int x mod int n))) *
         gauss_sum 1 *
         unity_root n (- int (m * nat (- int x mod int n)))"
          by clarsimp
      qed
      also have 2: "(∑x = 1..n. 1 / of_nat n * cnj (χ (nat (- int x mod int n))) *
          gauss_sum 1 * unity_root n (- int (m * nat (- int x mod int n)))) =
            (∑md = 0..n - 1. 1 / of_nat n * cnj (χ md) * gauss_sum 1 *
          unity_root n (- int (m * md)))"
       using sum.reindex_bij_betw[OF b, of "λmd. 1 / of_nat n * cnj (χ md) * gauss_sum 1 * unity_root n (- int (m * md))"]
       by blast
      also have 3: "… = (∑k = 0..n - 1.
        1 / of_nat n * cnj (χ k) * gauss_sum 1 *
        unity_root n (- int (m * k)))" by blast
      finally have "(∑k = 1..n. 1 / of_nat n * cnj (χ (nat (- int k mod int n))) *
        gauss_sum 1 * unity_root n (int (m * nat (int k mod int n)))) =
          (∑k = 0..n - 1.
        1 / of_nat n * cnj (χ k) * gauss_sum 1 *
        unity_root n (- int (m * k)))" using 1 2 3 by argo
      then show ?thesis by blast
    qed
  qed
  also have "… = (∑k = 1..n.
         1 / of_nat n * cnj (χ k) * gauss_sum 1 *
         unity_root n (- int (m * k)))"
  proof -
    let ?f = "(λk. 1 / of_nat n * cnj (χ k) * gauss_sum 1 * unity_root n (- int (m * k)))"
    have "?f 0 = 0" 
      using zero_eq_0 by auto
    have "?f n = 0" 
      using zero_eq_0 mod_periodic_arithmetic[OF dir_periodic_arithmetic, of n 0]
      by simp
    have "(∑n = 0..n - 1. ?f n) = (∑n = 1..n - 1. ?f n)"
      using sum_shift_lb_Suc0_0[of ?f, OF ‹?f 0 = 0›]
      by auto
    also have "… = (∑n = 1..n. ?f n)"
    proof (rule sum.mono_neutral_left,simp,simp,safe)
      fix i
      assume "i ∈ {1..n}" "i ∉ {1..n - 1}" 
      then have "i = n" using n by auto
      then show "1 / of_nat n * cnj (χ i) * gauss_sum 1 * unity_root n (- int (m * i)) = 0" 
        using ‹?f n = 0› by blast
    qed
    finally show ?thesis by blast
  qed
  also have "… = (∑k = 1..n. (τ / sqrt n) * cnj (χ k) * unity_root n (- int (m * k)))"
  proof (rule sum.cong,simp)
    fix x
    assume "x ∈ {1..n}"
    have "τ / sqrt (real n) = 1 / of_nat n * gauss_sum 1"
    proof -
      have "τ / sqrt (real n) = gauss_sum 1 / sqrt n / sqrt n"
        using assms by auto
      also have "… = gauss_sum 1 / (sqrt n * sqrt n)"
        by (subst divide_divide_eq_left,subst of_real_mult,blast) 
      also have "… = gauss_sum 1 / n" 
        using real_sqrt_mult_self by simp
      finally show ?thesis by simp
    qed
    then show 
     "1 / of_nat n * cnj (χ x) * gauss_sum 1 * unity_root n (- int (m * x)) =
      (τ / sqrt n) * cnj (χ x) * unity_root n (- int (m * x))" by simp
  qed
  also have "… = τ / sqrt (real n) *
         (∑k = 1..n. cnj (χ k) * unity_root n (- int (m * k)))"
  proof -
    have "(∑k = 1..n. τ / sqrt (real n) * cnj (χ k) * unity_root n (- int (m * k))) =
          (∑k = 1..n. τ / sqrt (real n) * (cnj (χ k) * unity_root n (- int (m * k))))" 
      by (rule sum.cong,simp, simp add: algebra_simps)
    also have "… = τ / sqrt (real n) * (∑k = 1..n. cnj (χ k) * unity_root n (- int (m * k)))"
      by (rule sum_distrib_left[symmetric])
    finally show ?thesis by blast
  qed

  finally show "χ m = (τ / sqrt (real n)) *
    (∑k=1..n. cnj (χ k) * unity_root n (- int m * int k))" by simp

  have 1: "norm (gauss_sum 1) = sqrt n" 
    using gauss_sum_1_mod_square_eq_k[OF primitive_encoding(2)]
    by (simp add: cmod_def)
  from assms have 2: "norm τ = norm (gauss_sum 1) / ∣sqrt n∣"
    by (simp add: norm_divide)
  show "norm τ = 1" using 1 2 n by simp
qed

unbundle vec_lambda_syntax

end