diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.field.cyclotomic.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.field.cyclotomic.html | 152 |
1 files changed, 0 insertions, 152 deletions
diff --git a/docs/htmldoc/mathcomp.field.cyclotomic.html b/docs/htmldoc/mathcomp.field.cyclotomic.html deleted file mode 100644 index 64a1afe..0000000 --- a/docs/htmldoc/mathcomp.field.cyclotomic.html +++ /dev/null @@ -1,152 +0,0 @@ -<!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/> - -<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#a659e4ae2d657a7a7479bd993753b74e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#a659e4ae2d657a7a7479bd993753b74e"><span class="id" title="notation">prod_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#a659e4ae2d657a7a7479bd993753b74e"><span class="id" title="notation">(</span></a><span class="id" title="var">k</span> <a class="idref" href="mathcomp.algebra.ssralg.html#a659e4ae2d657a7a7479bd993753b74e"><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#a659e4ae2d657a7a7479bd993753b74e"><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#a659e4ae2d657a7a7479bd993753b74e"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#a659e4ae2d657a7a7479bd993753b74e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">X</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#51dc792c356ca1a71a3094b50d6bb2fb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><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#663140372ac3b275aae871b74b140513"><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#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">)%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#a659e4ae2d657a7a7479bd993753b74e"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c94c2df86ca03f22f8f8b739cd7e1e88"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c94c2df86ca03f22f8f8b739cd7e1e88"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><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#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#228e85e3c31a939cba019f255574c875"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="mathcomp.ssreflect.eqtype.html#228e85e3c31a939cba019f255574c875"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#e809881bcf0cc80f806c17b9ef433187"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#e809881bcf0cc80f806c17b9ef433187"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#e809881bcf0cc80f806c17b9ef433187"><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#51dc792c356ca1a71a3094b50d6bb2fb"><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/V8.9.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#ad6a7217bc47606779ec5b6d2378a1dd"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.algebra.poly.html#ad6a7217bc47606779ec5b6d2378a1dd"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#ad6a7217bc47606779ec5b6d2378a1dd"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.algebra.poly.html#ad6a7217bc47606779ec5b6d2378a1dd"><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#e809881bcf0cc80f806c17b9ef433187"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#e809881bcf0cc80f806c17b9ef433187"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#e809881bcf0cc80f806c17b9ef433187"><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#51dc792c356ca1a71a3094b50d6bb2fb"><span class="id" title="notation">-</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#20f16c1d55d1e4ca9bb0e0513dd4b06a"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#20f16c1d55d1e4ca9bb0e0513dd4b06a"><span class="id" title="notation">prod_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#20f16c1d55d1e4ca9bb0e0513dd4b06a"><span class="id" title="notation">(</span></a><span class="id" title="var">d</span> <a class="idref" href="mathcomp.algebra.ssralg.html#20f16c1d55d1e4ca9bb0e0513dd4b06a"><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#20f16c1d55d1e4ca9bb0e0513dd4b06a"><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#663140372ac3b275aae871b74b140513"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#663140372ac3b275aae871b74b140513"><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#2242f6721707980eca939ec29164eab3"><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#663140372ac3b275aae871b74b140513"><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#8bf783530208799b469bca451a6c1096"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssrnum.html#8bf783530208799b469bca451a6c1096"><span class="id" title="notation">numDomainType</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#8bf783530208799b469bca451a6c1096"><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#8bf783530208799b469bca451a6c1096"><span class="id" title="notation">]</span></a>) : <span class="id" title="var">core</span>.<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#7f2a7ef2c63af7359b22787a9daf336e"><span class="id" title="notation">></span></a> 0)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">{</span></a><span class="id" title="var">z</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><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/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><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#ad6a7217bc47606779ec5b6d2378a1dd"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.algebra.poly.html#ad6a7217bc47606779ec5b6d2378a1dd"><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/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><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#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><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#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}</span></a> :=<br/> - <span class="id" title="keyword">let</span>: <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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#f953bf7095e0da1cb644443fd0e17d6d"><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="874b0df808ac9901a8162cab18629aee"><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#874b0df808ac9901a8162cab18629aee"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#874b0df808ac9901a8162cab18629aee"><span class="id" title="notation">Phi_n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c94c2df86ca03f22f8f8b739cd7e1e88"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c94c2df86ca03f22f8f8b739cd7e1e88"><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#ad6a7217bc47606779ec5b6d2378a1dd"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.algebra.poly.html#ad6a7217bc47606779ec5b6d2378a1dd"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#874b0df808ac9901a8162cab18629aee"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#874b0df808ac9901a8162cab18629aee"><span class="id" title="notation">Phi_n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#7f2a7ef2c63af7359b22787a9daf336e"><span class="id" title="notation">></span></a> 0)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#20f16c1d55d1e4ca9bb0e0513dd4b06a"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#20f16c1d55d1e4ca9bb0e0513dd4b06a"><span class="id" title="notation">prod_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#20f16c1d55d1e4ca9bb0e0513dd4b06a"><span class="id" title="notation">(</span></a><span class="id" title="var">d</span> <a class="idref" href="mathcomp.algebra.ssralg.html#20f16c1d55d1e4ca9bb0e0513dd4b06a"><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#20f16c1d55d1e4ca9bb0e0513dd4b06a"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#874b0df808ac9901a8162cab18629aee"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#874b0df808ac9901a8162cab18629aee"><span class="id" title="notation">Phi_d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.poly.html#e809881bcf0cc80f806c17b9ef433187"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#e809881bcf0cc80f806c17b9ef433187"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#e809881bcf0cc80f806c17b9ef433187"><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#51dc792c356ca1a71a3094b50d6bb2fb"><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#874b0df808ac9901a8162cab18629aee"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#874b0df808ac9901a8162cab18629aee"><span class="id" title="notation">Phi_0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#874b0df808ac9901a8162cab18629aee"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#874b0df808ac9901a8162cab18629aee"><span class="id" title="notation">Phi_n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><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#ad6a7217bc47606779ec5b6d2378a1dd"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.algebra.poly.html#ad6a7217bc47606779ec5b6d2378a1dd"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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 |