Library mathcomp.field.cyclotomic

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  
 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}.

(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.