:: Primitive Roots of Unity and Cyclotomic Polynomials
:: by Broderick Arneson and Piotr Rudnicki
::
:: Received December 30, 2003
:: Copyright (c) 2003-2016 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;
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;
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;