- -

Library mathcomp.field.cyclotomic

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- This file provides few basic properties of cyclotomic polynomials. - We define: - cyclotomic z n == the factorization of the nth cyclotomic polynomial in - a ring R in which z is an nth primitive root of unity. - 'Phi_n == the nth cyclotomic polynomial in int. - This library is quite limited, and should be extended in the future. In - particular the irreducibity of 'Phi_n is only stated indirectly, as the - fact that its embedding in the algebraics (algC) is the minimal polynomial - of an nth primitive root of unity. -

- -
-Set Implicit Arguments.
- -
-Import GRing.Theory Num.Theory.
-Local Open Scope ring_scope.
- -
-Section CyclotomicPoly.
- -
-Section Ring.
- -
-Variable R : ringType.
- -
-Definition cyclotomic (z : R) n :=
-  \prod_(k < n | coprime k n ) ('X - (z ^+ k )%:P ).
- -
-Lemma cyclotomic_monic z n : cyclotomic z n \is monic.
- -
-Lemma size_cyclotomic z n : size (cyclotomic z n) = (totient n ).+1.
- -
-End Ring.
- -
-Lemma separable_Xn_sub_1 (R : idomainType) n :
-  n %:R != 0 :> R → @separable_poly R ('X ^n - 1).
- -
-Section Field.
- -
-Variables (F : fieldType) (n : nat) (z : F).
-Hypothesis prim_z : n .-primitive_root z.
-Let n_gt0 := prim_order_gt0 prim_z.
- -
-Lemma root_cyclotomic x : root (cyclotomic z n) x = n .-primitive_root x.
- -
-Lemma prod_cyclotomic :
-  'X ^n - 1 = \prod_(d <- divisors n ) cyclotomic (z ^+ (n %/ d )) d.
- -
-End Field.
- -
-End CyclotomicPoly.
- -
- -
- -
-Local Hint Resolve (@intr_inj [numDomainType of algC ]) : core.
- -
-Lemma C_prim_root_exists n : (n > 0)%N → {z : algC | n .-primitive_root z }.
- -
-

- -

- (Integral) Cyclotomic polynomials. -

- -
-Definition Cyclotomic n : {poly int } :=
-  let: exist z _ := C_prim_root_exists (ltn0Sn n .-1) in
-  map_poly floorC (cyclotomic z n).
- -
-Notation "''Phi_' n" := (Cyclotomic n)
-  (at level 8, n at level 2, format "''Phi_' n").
- -
-Lemma Cyclotomic_monic n : 'Phi_n \is monic.
- -
-Lemma Cintr_Cyclotomic n z :
-  n .-primitive_root z → pZtoC 'Phi_n = cyclotomic z n.
- -
-Lemma prod_Cyclotomic n :
-  (n > 0)%N → \prod_(d <- divisors n ) 'Phi_d = 'X ^n - 1.
- -
-Lemma Cyclotomic0 : 'Phi_0 = 1.
- -
-Lemma size_Cyclotomic n : size 'Phi_n = (totient n ).+1.
- -
-Lemma minCpoly_cyclotomic n z :
-  n .-primitive_root z → minCpoly z = cyclotomic z n.
-