diff options
| author | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
| commit | ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch) | |
| tree | e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.field.cyclotomic.html | |
| parent | 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff) | |
generate the documentation for 1.7
Diffstat (limited to 'docs/htmldoc/mathcomp.field.cyclotomic.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.field.cyclotomic.html | 153 |
1 files changed, 153 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.field.cyclotomic.html b/docs/htmldoc/mathcomp.field.cyclotomic.html new file mode 100644 index 0000000..aa91124 --- /dev/null +++ b/docs/htmldoc/mathcomp.field.cyclotomic.html @@ -0,0 +1,153 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" +"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>mathcomp.field.cyclotomic</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library mathcomp.field.cyclotomic</h1> + +<div class="code"> +<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> + Distributed under the terms of CeCILL-B. *)</span><br/> +<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + 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. +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> + +<br/> +<span class="id" title="keyword">Import</span> <span class="id" title="var">GRing.Theory</span> <span class="id" title="var">Num.Theory</span>.<br/> +<span class="id" title="keyword">Local Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">ring_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="CyclotomicPoly"><span class="id" title="section">CyclotomicPoly</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="CyclotomicPoly.Ring"><span class="id" title="section">Ring</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="CyclotomicPoly.Ring.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="cyclotomic"><span class="id" title="definition">cyclotomic</span></a> (<span class="id" title="var">z</span> : <a class="idref" href="mathcomp.field.cyclotomic.html#CyclotomicPoly.Ring.R"><span class="id" title="variable">R</span></a>) <span class="id" title="var">n</span> :=<br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#f2061c5b083fb574331c7bf65b44ceb4"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#f2061c5b083fb574331c7bf65b44ceb4"><span class="id" title="notation">prod_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#f2061c5b083fb574331c7bf65b44ceb4"><span class="id" title="notation">(</span></a><span class="id" title="var">k</span> <a class="idref" href="mathcomp.algebra.ssralg.html#f2061c5b083fb574331c7bf65b44ceb4"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#f2061c5b083fb574331c7bf65b44ceb4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#f2061c5b083fb574331c7bf65b44ceb4"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#f2061c5b083fb574331c7bf65b44ceb4"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">X</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d70623330b2787db6b196e37db7d8f45"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">)%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#f2061c5b083fb574331c7bf65b44ceb4"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="cyclotomic_monic"><span class="id" title="lemma">cyclotomic_monic</span></a> <span class="id" title="var">z</span> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.field.cyclotomic.html#cyclotomic"><span class="id" title="definition">cyclotomic</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#e6408d45e92e642f7d1652448339ba09"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#e6408d45e92e642f7d1652448339ba09"><span class="id" title="notation">is</span></a> <a class="idref" href="mathcomp.algebra.poly.html#monic"><span class="id" title="definition">monic</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="size_cyclotomic"><span class="id" title="lemma">size_cyclotomic</span></a> <span class="id" title="var">z</span> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.field.cyclotomic.html#cyclotomic"><span class="id" title="definition">cyclotomic</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#totient"><span class="id" title="definition">totient</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">).+1</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.cyclotomic.html#CyclotomicPoly.Ring"><span class="id" title="section">Ring</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_Xn_sub_1"><span class="id" title="lemma">separable_Xn_sub_1</span></a> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.Exports.idomainType"><span class="id" title="abbreviation">idomainType</span></a>) <span class="id" title="var">n</span> :<br/> + <a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#9e45f909d1732d6d9e153b650829bccf"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="mathcomp.ssreflect.eqtype.html#9e45f909d1732d6d9e153b650829bccf"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> @<a class="idref" href="mathcomp.field.separable.html#separable_poly"><span class="id" title="definition">separable_poly</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#R"><span class="id" title="variable">R</span></a> (<a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d70623330b2787db6b196e37db7d8f45"><span class="id" title="notation">-</span></a> 1).<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="CyclotomicPoly.Field"><span class="id" title="section">Field</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="CyclotomicPoly.Field.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.fieldType"><span class="id" title="abbreviation">fieldType</span></a>) (<a name="CyclotomicPoly.Field.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="CyclotomicPoly.Field.z"><span class="id" title="variable">z</span></a> : <a class="idref" href="mathcomp.field.cyclotomic.html#F"><span class="id" title="variable">F</span></a>).<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="CyclotomicPoly.Field.prim_z"><span class="id" title="variable">prim_z</span></a> : <a class="idref" href="mathcomp.field.cyclotomic.html#CyclotomicPoly.Field.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.algebra.poly.html#92efb5ea268b6e2f9a125afe76aecbba"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.algebra.poly.html#92efb5ea268b6e2f9a125afe76aecbba"><span class="id" title="notation">primitive_root</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#CyclotomicPoly.Field.z"><span class="id" title="variable">z</span></a>.<br/> +<span class="id" title="keyword">Let</span> <a name="CyclotomicPoly.Field.n_gt0"><span class="id" title="variable">n_gt0</span></a> := <a class="idref" href="mathcomp.algebra.poly.html#prim_order_gt0"><span class="id" title="lemma">prim_order_gt0</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#CyclotomicPoly.Field.prim_z"><span class="id" title="variable">prim_z</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="root_cyclotomic"><span class="id" title="lemma">root_cyclotomic</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> (<a class="idref" href="mathcomp.field.cyclotomic.html#cyclotomic"><span class="id" title="definition">cyclotomic</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#CyclotomicPoly.Field.z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#CyclotomicPoly.Field.n"><span class="id" title="variable">n</span></a>) <a class="idref" href="mathcomp.field.cyclotomic.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#CyclotomicPoly.Field.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.algebra.poly.html#92efb5ea268b6e2f9a125afe76aecbba"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.algebra.poly.html#92efb5ea268b6e2f9a125afe76aecbba"><span class="id" title="notation">primitive_root</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="prod_cyclotomic"><span class="id" title="lemma">prod_cyclotomic</span></a> :<br/> + <a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#CyclotomicPoly.Field.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d70623330b2787db6b196e37db7d8f45"><span class="id" title="notation">-</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><span class="id" title="notation">prod_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><span class="id" title="notation">(</span></a><span class="id" title="var">d</span> <a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><span class="id" title="notation"><-</span></a> <a class="idref" href="mathcomp.ssreflect.prime.html#divisors"><span class="id" title="definition">divisors</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#CyclotomicPoly.Field.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#cyclotomic"><span class="id" title="definition">cyclotomic</span></a> (<a class="idref" href="mathcomp.field.cyclotomic.html#CyclotomicPoly.Field.z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#CyclotomicPoly.Field.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#df17451da28eb630dbb51b12706ba39e"><span class="id" title="notation">%/</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#d"><span class="id" title="variable">d</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">)</span></a>) <a class="idref" href="mathcomp.field.cyclotomic.html#d"><span class="id" title="variable">d</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.cyclotomic.html#CyclotomicPoly.Field"><span class="id" title="section">Field</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.cyclotomic.html#CyclotomicPoly"><span class="id" title="section">CyclotomicPoly</span></a>.<br/> + +<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Local Hint Resolve</span> (@<a class="idref" href="mathcomp.algebra.ssrint.html#intr_inj"><span class="id" title="definition">intr_inj</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#faa7b03f15fa8c0b383b6f3802b37e9e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssrnum.html#faa7b03f15fa8c0b383b6f3802b37e9e"><span class="id" title="notation">numDomainType</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#faa7b03f15fa8c0b383b6f3802b37e9e"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a><a class="idref" href="mathcomp.algebra.ssrnum.html#faa7b03f15fa8c0b383b6f3802b37e9e"><span class="id" title="notation">]</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="C_prim_root_exists"><span class="id" title="lemma">C_prim_root_exists</span></a> <span class="id" title="var">n</span> : (<a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#19ab5cfd7e4f60fa14f22b576013bd96"><span class="id" title="notation">></span></a> 0)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">{</span></a><span class="id" title="var">z</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.algebra.poly.html#92efb5ea268b6e2f9a125afe76aecbba"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.algebra.poly.html#92efb5ea268b6e2f9a125afe76aecbba"><span class="id" title="notation">primitive_root</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + (Integral) Cyclotomic polynomials. +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="Cyclotomic"><span class="id" title="definition">Cyclotomic</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.ssrint.html#int"><span class="id" title="inductive">int</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}</span></a> :=<br/> + <span class="id" title="keyword">let</span>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#exist"><span class="id" title="constructor">exist</span></a> <span class="id" title="var">z</span> <span class="id" title="var">_</span> := <a class="idref" href="mathcomp.field.cyclotomic.html#C_prim_root_exists"><span class="id" title="lemma">C_prim_root_exists</span></a> (<a class="idref" href="mathcomp.ssreflect.ssrnat.html#ltn0Sn"><span class="id" title="lemma">ltn0Sn</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a>) <span class="id" title="tactic">in</span><br/> + <a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.floorC"><span class="id" title="definition">floorC</span></a> (<a class="idref" href="mathcomp.field.cyclotomic.html#cyclotomic"><span class="id" title="definition">cyclotomic</span></a> <span class="id" title="var">z</span> <a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="84e794f5513e5917c9e68cdf3e4a2b12"><span class="id" title="notation">"</span></a>''Phi_' n" := (<a class="idref" href="mathcomp.field.cyclotomic.html#Cyclotomic"><span class="id" title="definition">Cyclotomic</span></a> <span class="id" title="var">n</span>)<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">n</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "''Phi_' n").<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Cyclotomic_monic"><span class="id" title="lemma">Cyclotomic_monic</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.field.cyclotomic.html#84e794f5513e5917c9e68cdf3e4a2b12"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#84e794f5513e5917c9e68cdf3e4a2b12"><span class="id" title="notation">Phi_n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#e6408d45e92e642f7d1652448339ba09"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#e6408d45e92e642f7d1652448339ba09"><span class="id" title="notation">is</span></a> <a class="idref" href="mathcomp.algebra.poly.html#monic"><span class="id" title="definition">monic</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Cintr_Cyclotomic"><span class="id" title="lemma">Cintr_Cyclotomic</span></a> <span class="id" title="var">n</span> <span class="id" title="var">z</span> :<br/> + <a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.algebra.poly.html#92efb5ea268b6e2f9a125afe76aecbba"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.algebra.poly.html#92efb5ea268b6e2f9a125afe76aecbba"><span class="id" title="notation">primitive_root</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#pZtoC"><span class="id" title="abbreviation">pZtoC</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#84e794f5513e5917c9e68cdf3e4a2b12"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#84e794f5513e5917c9e68cdf3e4a2b12"><span class="id" title="notation">Phi_n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#cyclotomic"><span class="id" title="definition">cyclotomic</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="prod_Cyclotomic"><span class="id" title="lemma">prod_Cyclotomic</span></a> <span class="id" title="var">n</span> :<br/> + (<a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#19ab5cfd7e4f60fa14f22b576013bd96"><span class="id" title="notation">></span></a> 0)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><span class="id" title="notation">prod_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><span class="id" title="notation">(</span></a><span class="id" title="var">d</span> <a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><span class="id" title="notation"><-</span></a> <a class="idref" href="mathcomp.ssreflect.prime.html#divisors"><span class="id" title="definition">divisors</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#84e794f5513e5917c9e68cdf3e4a2b12"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#84e794f5513e5917c9e68cdf3e4a2b12"><span class="id" title="notation">Phi_d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d70623330b2787db6b196e37db7d8f45"><span class="id" title="notation">-</span></a> 1.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Cyclotomic0"><span class="id" title="lemma">Cyclotomic0</span></a> : <a class="idref" href="mathcomp.field.cyclotomic.html#84e794f5513e5917c9e68cdf3e4a2b12"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#84e794f5513e5917c9e68cdf3e4a2b12"><span class="id" title="notation">Phi_0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="size_Cyclotomic"><span class="id" title="lemma">size_Cyclotomic</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#84e794f5513e5917c9e68cdf3e4a2b12"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#84e794f5513e5917c9e68cdf3e4a2b12"><span class="id" title="notation">Phi_n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#totient"><span class="id" title="definition">totient</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">).+1</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="minCpoly_cyclotomic"><span class="id" title="lemma">minCpoly_cyclotomic</span></a> <span class="id" title="var">n</span> <span class="id" title="var">z</span> :<br/> + <a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.algebra.poly.html#92efb5ea268b6e2f9a125afe76aecbba"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.algebra.poly.html#92efb5ea268b6e2f9a125afe76aecbba"><span class="id" title="notation">primitive_root</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.minCpoly"><span class="id" title="definition">minCpoly</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#cyclotomic"><span class="id" title="definition">cyclotomic</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#n"><span class="id" title="variable">n</span></a>.<br/> +</div> +</div> + +<div id="footer"> +<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> +</div> + +</div> + +</body> +</html>
\ No newline at end of file |