Library mathcomp.field.cyclotomic
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div choice fintype tuple finfun bigop prime.
From mathcomp Require Import ssralg poly finset fingroup finalg zmodp cyclic.
From mathcomp Require Import ssrnum ssrint polydiv rat intdiv mxpoly.
From mathcomp Require Import vector falgebra fieldext separable galois algC.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div choice fintype tuple finfun bigop prime.
From mathcomp Require Import ssralg poly finset fingroup finalg zmodp cyclic.
From mathcomp Require Import ssrnum ssrint polydiv rat intdiv mxpoly.
From mathcomp Require Import vector falgebra fieldext separable galois algC.
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 Notation ZtoQ := (intr : int → rat).
Local Notation ZtoC := (intr : int → algC).
Local Notation QtoC := (ratr : rat → algC).
Local Notation intrp := (map_poly intr).
Local Notation pZtoQ := (map_poly ZtoQ).
Local Notation pZtoC := (map_poly ZtoC).
Local Notation pQtoC := (map_poly ratr).
Local Definition algC_intr_inj := @intr_inj [numDomainType of algC].
#[local] Hint Resolve algC_intr_inj : core.
Local Notation QtoC_M := (ratr_rmorphism [numFieldType 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.