Library mathcomp.field.cyclotomic
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ 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]).
+ +
+Lemma C_prim_root_exists n : (n > 0)%N → {z : algC | n.-primitive_root z}.
+ +
+
+
++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]).
+ +
+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.
+
++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.
+