:: Primitive Roots of Unity and Cyclotomic Polynomials
::  by Broderick Arneson and Piotr Rudnicki
::
:: Received December 30, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, XBOOLE_0, XXREAL_0, CARD_1, ARYTM_3, NAT_1,
      FINSEQ_1, RELAT_1, FUNCT_1, TARSKI, COMPLFLD, COMPLEX1, PARTFUN1, CARD_3,
      STRUCT_0, REAL_1, ORDINAL4, FINSET_1, UPROOTS, ARYTM_1, POLYNOM2,
      AFINSQ_1, GROUP_1, INT_1, HAHNBAN1, SQUARE_1, POWER, SIN_COS, BINOP_1,
      ALGSTR_0, FINSEQ_2, MOD_2, VECTSP_1, VECTSP_2, REALSET1, ZFMISC_1,
      SUPINF_2, COMPTRIG, RAT_1, PREPOWER, NEWTON, XCMPLX_0, INT_2, BINOP_2,
      GROUP_2, POLYNOM1, POLYNOM3, FUNCT_4, ALGSEQ_1, VALUED_0, POLYNOM5,
      SGRAPH1, PRE_POLY, GRAPH_2, MESFUNC1, UNIROOTS;
 notations TARSKI, XBOOLE_0, SUBSET_1, REALSET1, CARD_1, ORDINAL1, NUMBERS,
      XREAL_0, ZFMISC_1, XXREAL_0, XCMPLX_0, COMPLEX1, REAL_1, SQUARE_1, INT_1,
      INT_2, NAT_D, PREPOWER, POWER, BINOP_1, RELAT_1, FUNCT_1, PARTFUN1,
      FUNCT_2, FINSEQ_1, RAT_1, DOMAIN_1, FINSET_1, BINOP_2, RVSUM_1, STRUCT_0,
      ALGSTR_0, VECTSP_2, VECTSP_1, GROUP_4, ALGSEQ_1, COMPLFLD, HAHNBAN1,
      POLYNOM3, POLYNOM4, POLYNOM5, COMPTRIG, GROUP_2, NEWTON, GROUP_1, MOD_2,
      GRAPH_2, PRE_POLY, FVSUM_1, UPROOTS, SIN_COS, FUNCT_7, FINSEQ_2,
      FINSEQ_6;
 constructors WELLORD2, BINOP_1, REAL_1, SQUARE_1, NAT_D, FINSEQOP, FINSOP_1,
      RVSUM_1, PREPOWER, POWER, REALSET1, SIN_COS, GROUP_4, MOD_2, MATRIX_1,
      HAHNBAN1, GRAPH_2, POLYNOM4, POLYNOM5, UPROOTS, RECDEF_1, BINOP_2,
      RELSET_1, PBOOLE, FUNCT_7, NEWTON, FVSUM_1, ALGSEQ_1, FINSEQ_6;
 registrations RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
      XREAL_0, NAT_1, INT_1, BINOP_2, CARD_1, MEMBERED, FINSEQ_1, FINSEQ_2,
      REALSET1, WSIERP_1, STRUCT_0, GROUP_1, VECTSP_1, COMPLFLD, QUOFIELD,
      POLYNOM3, POLYNOM5, VALUED_0, ALGSTR_0, POWER, RELSET_1, PRE_POLY,
      PREPOWER, SQUARE_1, NEWTON, SIN_COS, ORDINAL1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;


begin

scheme :: UNIROOTS:sch 1
  CompIndNE { P[non zero Nat] } : for k being non zero Element of NAT holds
  P[k]
provided
 for k being non zero Element of NAT st for n being non zero
Element of NAT st n < k holds P[n] holds P[k];

theorem :: UNIROOTS:1
  for f being FinSequence st 1 <= len f holds f | Seg 1 = <*f.1*>;

theorem :: UNIROOTS:2
  for f being FinSequence of F_Complex, g being FinSequence of REAL
st len f = len g & for i being Element of NAT st i in dom f holds |. f/.i .| =
  g.i holds |. Product f .| = Product g;

theorem :: UNIROOTS:3
  for s being non empty finite Subset of F_Complex, x being Element
  of F_Complex, r being FinSequence of REAL st len r = card s & for i being
  Element of NAT, c being Element of F_Complex st i in dom r & c = (canFS(s)).i
  holds r.i = |.x-c.| holds |.eval(poly_with_roots((s,1)-bag),x).| = Product(r)
;

theorem :: UNIROOTS:4
  for f being FinSequence of F_Complex st for i being Element of
  NAT st i in dom f holds f.i is integer holds Sum f is integer;

theorem :: UNIROOTS:5
  for x, y being Element of F_Complex, r1, r2 being Real st r1=x & r2=y
  holds r1*r2 = x*y & r1+r2=x+y;

theorem :: UNIROOTS:6
  for q being Real st q > 0 for r being Element of F_Complex st |.r
  .| = 1 & r <> [**1,0**] holds |.[**q, 0**] - r.| > q - 1;

theorem :: UNIROOTS:7
  for ps being non empty FinSequence of REAL, x being Real st x >=
1 & for i being Element of NAT st i in dom ps holds ps.i > x holds Product(ps)
  > x;

theorem :: UNIROOTS:8
  for n being Element of NAT holds 1_F_Complex = (power F_Complex)
  .(1_F_Complex,n);

theorem :: UNIROOTS:9
  for n, i being Nat holds cos((2*PI*i)/n) = cos((2*PI*
  (i mod n))/n) & sin((2*PI*i)/n) = sin((2*PI*(i mod n))/n);

theorem :: UNIROOTS:10
  for n, i being Nat holds [** cos((2*PI*i)/n), sin((2*
  PI*i)/n)**] = [** cos((2*PI*(i mod n))/n), sin((2*PI*(i mod n))/n) **];

theorem :: UNIROOTS:11
  for n, i, j being Element of NAT holds [** cos((2*PI*i)/n),sin((
  2*PI*i)/n) **]*[** cos((2*PI*j)/n),sin((2*PI*j)/n) **] = [** cos((2*PI*((i+j)
  mod n))/n), sin((2*PI*((i+j)mod n))/n)**];

theorem :: UNIROOTS:12
  for L being unital associative non empty multMagma, x being
  Element of L, n,m being Nat holds (power L).(x,n*m) = (power L).((
  power L).(x,n),m);

theorem :: UNIROOTS:13
  for n being Element of NAT, x being Element of F_Complex st x is
  Integer holds (power F_Complex).(x,n) is Integer;

theorem :: UNIROOTS:14
  for F being FinSequence of F_Complex st for i being Element of
  NAT st i in dom F holds F.i is Integer holds Sum F is Integer;

registration
  cluster finite for Field;
  cluster finite for Skew-Field;
end;

begin :: Multiplicative group of a skew field

definition
  let R be Skew-Field;
  func MultGroup R -> strict Group means
:: UNIROOTS:def 1

  the carrier of it = NonZero R
  & the multF of it = (the multF of R)||the carrier of it;
end;

theorem :: UNIROOTS:15 :: WEDDWITT
  for R being Skew-Field holds the carrier of R = (the carrier of
  MultGroup R) \/ {0.R};

theorem :: UNIROOTS:16
  for R being Skew-Field, a, b being Element of R, c, d being
  Element of MultGroup R st a = c & b = d holds c*d = a*b;

theorem :: UNIROOTS:17
  for R being Skew-Field holds 1_R = 1_MultGroup R;

registration
  let R be finite Skew-Field;
  cluster MultGroup R -> finite;
end;

theorem :: UNIROOTS:18 :: WEDDWITT
  for R being finite Skew-Field holds card MultGroup R = card R - 1;

theorem :: UNIROOTS:19
  for R being Skew-Field, s being set st s in the carrier of
  MultGroup R holds s in the carrier of R;

theorem :: UNIROOTS:20
  for R being Skew-Field holds the carrier of MultGroup R c= the carrier of R;

begin :: Roots of 1

definition
  let n be non zero Element of NAT;
  func n-roots_of_1 -> Subset of F_Complex equals
:: UNIROOTS:def 2
  { x where x is Element of
  F_Complex : x is CRoot of n,1_F_Complex };
end;

theorem :: UNIROOTS:21
  for n being non zero Element of NAT, x being Element of
  F_Complex holds x in n-roots_of_1 iff x is CRoot of n,1_F_Complex;

theorem :: UNIROOTS:22
  for n being non zero Element of NAT holds 1_F_Complex in n -roots_of_1;

theorem :: UNIROOTS:23
  for n being non zero Element of NAT, x being Element of
  F_Complex st x in n-roots_of_1 holds |.x.| = 1;

theorem :: UNIROOTS:24
  for n being non zero Element of NAT for x being Element of
F_Complex holds x in n-roots_of_1 iff ex k being Element of NAT st x = [** cos(
  (2*PI*k)/n), sin((2*PI*k)/n) **];

theorem :: UNIROOTS:25
  for n being non zero Element of NAT for x,y being Element of
  COMPLEX st x in n-roots_of_1 & y in n-roots_of_1 holds x*y in n-roots_of_1;

theorem :: UNIROOTS:26
  for n being non zero Element of NAT holds n-roots_of_1 = {[**
  cos((2*PI*k)/n),sin((2*PI*k)/n)**] where k is Element of NAT: k < n };

theorem :: UNIROOTS:27
  for n being non zero Element of NAT holds card (n-roots_of_1) = n;

registration
  let n be non zero Element of NAT;
  cluster n-roots_of_1 -> non empty;
  cluster n-roots_of_1 -> finite;
end;

theorem :: UNIROOTS:28
  for n, ni being non zero Element of NAT st ni divides n holds
  ni-roots_of_1 c= n-roots_of_1;

theorem :: UNIROOTS:29
  for R being Skew-Field, x being Element of MultGroup R, y being
Element of R st y = x for k being Nat holds (power (MultGroup R)).(x
  ,k) = (power R).(y,k);

theorem :: UNIROOTS:30
  for n being non zero Element of NAT, x being Element of
  MultGroup F_Complex st x in n-roots_of_1 holds x is not being_of_order_0;

theorem :: UNIROOTS:31
  for n being non zero Element of NAT, k being Element of NAT, x
being Element of MultGroup F_Complex st x = [** cos((2*PI*k)/n), sin((2*PI*k)/n
  ) **] holds ord x = n div (k gcd n);

theorem :: UNIROOTS:32
  for n being non zero Element of NAT holds n-roots_of_1 c= the
  carrier of MultGroup F_Complex;

theorem :: UNIROOTS:33
  for n being non zero Element of NAT holds ex x being Element of
  MultGroup F_Complex st ord x = n;

theorem :: UNIROOTS:34
  for n being non zero Element of NAT, x being Element of
  MultGroup F_Complex holds ord x divides n iff x in n-roots_of_1;

theorem :: UNIROOTS:35
  for n being non zero Element of NAT holds n-roots_of_1 = { x
  where x is Element of MultGroup F_Complex : ord x divides n};

theorem :: UNIROOTS:36
  for n being non zero Element of NAT, x being set holds x in n
  -roots_of_1 iff ex y being Element of MultGroup F_Complex st x = y & ord y
  divides n;

definition
  let n be non zero Element of NAT;
  func n-th_roots_of_1 -> strict Group means
:: UNIROOTS:def 3

  the carrier of it = n
  -roots_of_1 & the multF of it = (the multF of F_Complex)||(n-roots_of_1);
end;

theorem :: UNIROOTS:37
  for n being non zero Element of NAT holds n-th_roots_of_1 is Subgroup
  of MultGroup F_Complex;

begin :: The unital polynomial x^n -1

definition
  let n be non zero Nat, L be left_unital non empty doubleLoopStr;
  func unital_poly(L,n) -> Polynomial of L equals
:: UNIROOTS:def 4
  0_.(L)+*(0,-(1_L))+*(n,1_L);
end;

theorem :: UNIROOTS:38
  for L being left_unital non empty doubleLoopStr for n being
non zero Element of NAT holds unital_poly(L,n).0 = -1_L & unital_poly(L,n).n =
  1_L;

theorem :: UNIROOTS:39
  for L being left_unital non empty doubleLoopStr for n being
  non zero Nat, i being Nat st i <> 0 & i <> n holds unital_poly(L,n).i = 0.L;

theorem :: UNIROOTS:40
  for L being non degenerated well-unital non empty doubleLoopStr
  , n being non zero Element of NAT holds len unital_poly(L,n) = n+1;

registration
  let L be non degenerated well-unital non empty doubleLoopStr, n be non
  zero Element of NAT;
  cluster unital_poly(L,n) -> non-zero;
end;

theorem :: UNIROOTS:41
  for n being non zero Element of NAT for x being Element of
F_Complex holds eval(unital_poly(F_Complex,n), x) = (power F_Complex).(x,n) - 1
;

theorem :: UNIROOTS:42
  for n being non zero Element of NAT holds Roots unital_poly(
  F_Complex, n) = n-roots_of_1;

theorem :: UNIROOTS:43
  for n being Element of NAT, z being Element of F_Complex st z is
  Real ex x being Real st x = z & (power F_Complex).(z,n) = x |^ n;

theorem :: UNIROOTS:44
  for n being non zero Element of NAT for x being Real ex y being
Element of F_Complex st y = x & eval(unital_poly(F_Complex,n),y) = (x |^ n) - 1
;

theorem :: UNIROOTS:45
  for n being non zero Element of NAT holds BRoots unital_poly(
  F_Complex, n) = (n-roots_of_1, 1)-bag;

theorem :: UNIROOTS:46
  for n being non zero Element of NAT holds unital_poly(F_Complex
  , n) = poly_with_roots((n-roots_of_1, 1)-bag);

theorem :: UNIROOTS:47
  for n being non zero Element of NAT, i being Element of
  F_Complex st i is Integer holds eval(unital_poly(F_Complex, n), i) is Integer
;

begin :: Cyclotomic Polynomials

definition
  let d be non zero Nat;
  func cyclotomic_poly d -> Polynomial of F_Complex means
:: UNIROOTS:def 5

  ex s being
non empty finite Subset of F_Complex st s = { y where y is Element of MultGroup
  F_Complex : ord y = d } & it = poly_with_roots((s,1)-bag);
end;

theorem :: UNIROOTS:48
  cyclotomic_poly(1) = <%-1_F_Complex, 1_F_Complex %>;

theorem :: UNIROOTS:49
  for n being non zero Element of NAT, f being FinSequence of (
  the carrier of Polynom-Ring F_Complex) st len f = n & for i being non zero
Element of NAT st i in dom f holds (not i divides n implies f.i = <%1_F_Complex
  %>) & (i divides n implies f.i = cyclotomic_poly(i)) holds unital_poly(
  F_Complex,n) = Product(f);

theorem :: UNIROOTS:50
  for n being non zero Element of NAT ex f being FinSequence of (
the carrier of Polynom-Ring F_Complex), p being Polynomial of F_Complex st p =
Product(f) & dom f = Seg n & (for i being non zero Element of NAT st i in Seg
n holds (not i divides n or i = n implies f.i = <%1_F_Complex%>) & (i divides n
  & i <> n implies f.i = cyclotomic_poly(i))) & unital_poly(F_Complex,n) = (
  cyclotomic_poly n)*'p;

theorem :: UNIROOTS:51
  for d being non zero Element of NAT, i being Element of NAT
  holds ((cyclotomic_poly d).0 = 1 or (cyclotomic_poly d).0 = -1) & (
  cyclotomic_poly d).i is integer;

theorem :: UNIROOTS:52  :: WEDDWITT
  for d being non zero Element of NAT, z being Element of
  F_Complex st z is Integer holds eval(cyclotomic_poly(d),z) is Integer;

theorem :: UNIROOTS:53
  for n, ni being non zero Element of NAT, f being FinSequence of
(the carrier of Polynom-Ring F_Complex), s being finite Subset of F_Complex st
s = {y where y is Element of MultGroup F_Complex : ord y divides n & not ord y
divides ni & ord y <> n} & dom f = Seg n & for i being non zero Element of NAT
st i in dom f holds (not i divides n or i divides ni or i = n implies f.i = <%
  1_F_Complex%>) & (i divides n & not i divides ni & i <> n implies f.i =
  cyclotomic_poly(i)) holds Product(f) = poly_with_roots((s,1)-bag);

theorem :: UNIROOTS:54
  for n, ni being non zero Element of NAT st ni < n & ni divides
  n ex f being FinSequence of (the carrier of Polynom-Ring F_Complex), p being
  Polynomial of F_Complex st p = Product(f) & dom f = Seg n & (for i being non
zero Element of NAT st i in Seg n holds (not i divides n or i divides ni or i
  = n implies f.i = <%1_F_Complex%>) & (i divides n & not i divides ni & i <> n
  implies f.i = cyclotomic_poly(i))) & unital_poly(F_Complex,n) = unital_poly(
  F_Complex,ni)*'(cyclotomic_poly n)*'p;

theorem :: UNIROOTS:55
  for i being Integer, c being Element of F_Complex, f being
  FinSequence of (the carrier of Polynom-Ring F_Complex), p being Polynomial of
F_Complex st p = Product(f) & c = i & for i being non zero Element of NAT st i
in dom f holds f.i = <%1_F_Complex%> or f.i = cyclotomic_poly(i) holds eval(p,c
  ) is integer;

theorem :: UNIROOTS:56
  for n being non zero Element of NAT, j, k, q being Integer, qc
  being Element of F_Complex st qc = q & j = eval(cyclotomic_poly(n),qc) & k =
  eval(unital_poly(F_Complex, n),qc) holds j divides k;

theorem :: UNIROOTS:57
  for n,ni being non zero Element of NAT, q being Integer st ni <
  n & ni divides n for qc being Element of F_Complex st qc = q for j,k,l being
Integer st j = eval(cyclotomic_poly(n),qc) & k = eval(unital_poly(F_Complex, n)
  ,qc) & l = eval(unital_poly(F_Complex, ni),qc) holds j divides (k div l);

theorem :: UNIROOTS:58
  for n,q being non zero Element of NAT, qc being Element of F_Complex
  st qc = q for j being Integer st j = eval(cyclotomic_poly(n),qc) holds j
  divides (q |^ n - 1);

theorem :: UNIROOTS:59
  for n,ni,q being non zero Element of NAT st ni < n & ni divides n for
  qc being Element of F_Complex st qc = q for j being Integer st j = eval(
  cyclotomic_poly(n),qc) holds j divides ((q |^ n - 1) div (q |^ ni - 1));

theorem :: UNIROOTS:60
  for n being non zero Element of NAT st 1 < n for q being Element of
NAT st 1 < q for qc being Element of F_Complex st qc = q for i being Integer st
  i = eval(cyclotomic_poly(n),qc) holds |.i.| > q - 1;