diff options
| author | Enrico Tassi | 2019-05-22 13:43:08 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-05-22 15:34:14 +0200 |
| commit | 748d716efb2f2f75946c8386e441ce1789806a39 (patch) | |
| tree | fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/mathcomp.field.cyclotomic.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/mathcomp.field.cyclotomic.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.field.cyclotomic.html | 39 |
1 files changed, 19 insertions, 20 deletions
diff --git a/docs/htmldoc/mathcomp.field.cyclotomic.html b/docs/htmldoc/mathcomp.field.cyclotomic.html index aa91124..64a1afe 100644 --- a/docs/htmldoc/mathcomp.field.cyclotomic.html +++ b/docs/htmldoc/mathcomp.field.cyclotomic.html @@ -21,7 +21,6 @@ <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> @@ -57,35 +56,35 @@ <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/> + <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/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/> +<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/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/> +<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#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/> + <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/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">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/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/> +<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#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/> + <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/> @@ -98,10 +97,10 @@ <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/> +<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#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/> +<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> @@ -112,34 +111,34 @@ <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/> +<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="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="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#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/> +<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#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/> + <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#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/> + (<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#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/> +<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#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/> +<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#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/> + <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> |