diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.algebra.zmodp.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.algebra.zmodp.html | 433 |
1 files changed, 0 insertions, 433 deletions
diff --git a/docs/htmldoc/mathcomp.algebra.zmodp.html b/docs/htmldoc/mathcomp.algebra.zmodp.html deleted file mode 100644 index f8d448b..0000000 --- a/docs/htmldoc/mathcomp.algebra.zmodp.html +++ /dev/null @@ -1,433 +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.algebra.zmodp</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.algebra.zmodp</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"> - Definition of the additive group and ring Zp, represented as 'I_p -<div class="paragraph"> </div> - - Definitions: - From fintype.v: - 'I_p == the subtype of integers less than p, taken here as the type of - the integers mod p. - This file: - inZp == the natural projection from nat into the integers mod p, - represented as 'I_p. Here p is implicit, but MUST be of the - form n.+1. - The operations: - Zp0 == the identity element for addition - Zp1 == the identity element for multiplication, and a generator of - additive group - Zp_opp == inverse function for addition - Zp_add == addition - Zp_mul == multiplication - Zp_inv == inverse function for multiplication - Note that while 'I_n.+1 has canonical finZmodType and finGroupType - structures, only 'I_n.+2 has a canonical ring structure (it has, in fact, - a canonical finComUnitRing structure), and hence an associated - multiplicative unit finGroupType. To mitigate the issues caused by the - trivial "ring" (which is, indeed is NOT a ring in the ssralg/finalg - formalization), we define additional notation: - 'Z_p == the type of integers mod (max p 2); this is always a proper - ring, by constructions. Note that 'Z_p is provably equal to - 'I_p if p > 1, and convertible to 'I_p if p is of the form - n.+2. - Zp p == the subgroup of integers mod (max p 1) in 'Z_p; this is thus - is thus all of 'Z_p if p > 1, and else the trivial group. - units_Zp p == the group of all units of 'Z_p -- i.e., the group of - (multiplicative) automorphisms of Zp p. - We show that Zp and units_Zp are abelian, and compute their orders. - We use a similar technique to represent the prime fields: - 'F_p == the finite field of integers mod the first prime divisor of - maxn p 2. This is provably equal to 'Z_p and 'I_p if p is - provably prime, and indeed convertible to the above if p is - a concrete prime such as 2, 5 or 23. - Note finally that due to the canonical structures it is possible to use - 0%R instead of Zp0, and 1%R instead of Zp1 (for the latter, p must be of - the form n.+2, and 1%R : nat will simplify to 1%N). -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> - -<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="ZpDef"><span class="id" title="section">ZpDef</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - -<div class="paragraph"> </div> - - Mod p arithmetic on the finite set {0, 1, 2, ..., p - 1} - -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="ZpDef.p'"><span class="id" title="variable">p'</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>.<br/> - -<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - Standard injection; val (inZp i) = i %% p -</div> -<div class="code"> -<span class="id" title="keyword">Definition</span> <a name="inZp"><span class="id" title="definition">inZp</span></a> <span class="id" title="var">i</span> := <a class="idref" href="mathcomp.ssreflect.fintype.html#Ordinal"><span class="id" title="constructor">Ordinal</span></a> (<a class="idref" href="mathcomp.ssreflect.div.html#ltn_pmod"><span class="id" title="lemma">ltn_pmod</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#i"><span class="id" title="variable">i</span></a> (<a class="idref" href="mathcomp.ssreflect.ssrnat.html#ltn0Sn"><span class="id" title="lemma">ltn0Sn</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#ZpDef.p'"><span class="id" title="variable">p'</span></a>)).<br/> -<span class="id" title="keyword">Lemma</span> <a name="modZp"><span class="id" title="lemma">modZp</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#e3d79e08e7e529cc9ef532e000103386"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#p"><span class="id" title="abbreviation">p</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.zmodp.html#x"><span class="id" title="variable">x</span></a>.<br/> - <span class="id" title="keyword">Lemma</span> <a name="valZpK"><span class="id" title="lemma">valZpK</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.zmodp.html#inZp"><span class="id" title="definition">inZp</span></a> <a class="idref" href="mathcomp.algebra.zmodp.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.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - Operations -</div> -<div class="code"> -<span class="id" title="keyword">Definition</span> <a name="Zp0"><span class="id" title="definition">Zp0</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a> := <a class="idref" href="mathcomp.ssreflect.fintype.html#ord0"><span class="id" title="definition">ord0</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="Zp1"><span class="id" title="definition">Zp1</span></a> := <a class="idref" href="mathcomp.algebra.zmodp.html#inZp"><span class="id" title="definition">inZp</span></a> 1.<br/> -<span class="id" title="keyword">Definition</span> <a name="Zp_opp"><span class="id" title="definition">Zp_opp</span></a> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.algebra.zmodp.html#inZp"><span class="id" title="definition">inZp</span></a> (<a class="idref" href="mathcomp.algebra.zmodp.html#p"><span class="id" title="abbreviation">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#7825ccc99f23b0d30c9d40c317ba7af0"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a>).<br/> -<span class="id" title="keyword">Definition</span> <a name="Zp_add"><span class="id" title="definition">Zp_add</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> := <a class="idref" href="mathcomp.algebra.zmodp.html#inZp"><span class="id" title="definition">inZp</span></a> (<a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#y"><span class="id" title="variable">y</span></a>).<br/> -<span class="id" title="keyword">Definition</span> <a name="Zp_mul"><span class="id" title="definition">Zp_mul</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> := <a class="idref" href="mathcomp.algebra.zmodp.html#inZp"><span class="id" title="definition">inZp</span></a> (<a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#y"><span class="id" title="variable">y</span></a>).<br/> -<span class="id" title="keyword">Definition</span> <a name="Zp_inv"><span class="id" title="definition">Zp_inv</span></a> <span class="id" title="var">x</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#p"><span class="id" title="abbreviation">p</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#inZp"><span class="id" title="definition">inZp</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.div.html#egcdn"><span class="id" title="definition">egcdn</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#p"><span class="id" title="abbreviation">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">).1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - Additive group structure. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_add0z"><span class="id" title="lemma">Zp_add0z</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#left_id"><span class="id" title="definition">left_id</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp0"><span class="id" title="definition">Zp0</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_add"><span class="id" title="definition">Zp_add</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_addNz"><span class="id" title="lemma">Zp_addNz</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#left_inverse"><span class="id" title="definition">left_inverse</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp0"><span class="id" title="definition">Zp0</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_opp"><span class="id" title="definition">Zp_opp</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_add"><span class="id" title="definition">Zp_add</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_addA"><span class="id" title="lemma">Zp_addA</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#associative"><span class="id" title="definition">associative</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_add"><span class="id" title="definition">Zp_add</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_addC"><span class="id" title="lemma">Zp_addC</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#commutative"><span class="id" title="definition">commutative</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_add"><span class="id" title="definition">Zp_add</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Zp_zmodMixin"><span class="id" title="definition">Zp_zmodMixin</span></a> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Exports.ZmodMixin"><span class="id" title="abbreviation">ZmodMixin</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_addA"><span class="id" title="lemma">Zp_addA</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_addC"><span class="id" title="lemma">Zp_addC</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_add0z"><span class="id" title="lemma">Zp_add0z</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_addNz"><span class="id" title="lemma">Zp_addNz</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_zmodType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Exports.ZmodType"><span class="id" title="abbreviation">ZmodType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_zmodMixin"><span class="id" title="definition">Zp_zmodMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_finZmodType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.finalg.html#144f70011c058d1c741eaa431b4b8944"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#144f70011c058d1c741eaa431b4b8944"><span class="id" title="notation">finZmodType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#144f70011c058d1c741eaa431b4b8944"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a><a class="idref" href="mathcomp.algebra.finalg.html#144f70011c058d1c741eaa431b4b8944"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_baseFinGroupType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.finalg.html#d6b25f501b9fb5e9b743073d52f24511"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#d6b25f501b9fb5e9b743073d52f24511"><span class="id" title="notation">baseFinGroupType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#d6b25f501b9fb5e9b743073d52f24511"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#d6b25f501b9fb5e9b743073d52f24511"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#d6b25f501b9fb5e9b743073d52f24511"><span class="id" title="notation">+%</span></a><a class="idref" href="mathcomp.algebra.finalg.html#d6b25f501b9fb5e9b743073d52f24511"><span class="id" title="notation">R</span></a><a class="idref" href="mathcomp.algebra.finalg.html#d6b25f501b9fb5e9b743073d52f24511"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_finGroupType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.finalg.html#a37f16a335f7a3ac65f83e3545c3e50c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#a37f16a335f7a3ac65f83e3545c3e50c"><span class="id" title="notation">finGroupType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#a37f16a335f7a3ac65f83e3545c3e50c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#a37f16a335f7a3ac65f83e3545c3e50c"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#a37f16a335f7a3ac65f83e3545c3e50c"><span class="id" title="notation">+%</span></a><a class="idref" href="mathcomp.algebra.finalg.html#a37f16a335f7a3ac65f83e3545c3e50c"><span class="id" title="notation">R</span></a><a class="idref" href="mathcomp.algebra.finalg.html#a37f16a335f7a3ac65f83e3545c3e50c"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - Ring operations -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_mul1z"><span class="id" title="lemma">Zp_mul1z</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#left_id"><span class="id" title="definition">left_id</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp1"><span class="id" title="definition">Zp1</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_mul"><span class="id" title="definition">Zp_mul</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_mulC"><span class="id" title="lemma">Zp_mulC</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#commutative"><span class="id" title="definition">commutative</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_mul"><span class="id" title="definition">Zp_mul</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_mulz1"><span class="id" title="lemma">Zp_mulz1</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#right_id"><span class="id" title="definition">right_id</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp1"><span class="id" title="definition">Zp1</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_mul"><span class="id" title="definition">Zp_mul</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_mulA"><span class="id" title="lemma">Zp_mulA</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#associative"><span class="id" title="definition">associative</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_mul"><span class="id" title="definition">Zp_mul</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_mul_addr"><span class="id" title="lemma">Zp_mul_addr</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#right_distributive"><span class="id" title="definition">right_distributive</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_mul"><span class="id" title="definition">Zp_mul</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_add"><span class="id" title="definition">Zp_add</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_mul_addl"><span class="id" title="lemma">Zp_mul_addl</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#left_distributive"><span class="id" title="definition">left_distributive</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_mul"><span class="id" title="definition">Zp_mul</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_add"><span class="id" title="definition">Zp_add</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_mulVz"><span class="id" title="lemma">Zp_mulVz</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#p"><span class="id" title="abbreviation">p</span></a> <a class="idref" href="mathcomp.algebra.zmodp.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#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_mul"><span class="id" title="definition">Zp_mul</span></a> (<a class="idref" href="mathcomp.algebra.zmodp.html#Zp_inv"><span class="id" title="definition">Zp_inv</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.algebra.zmodp.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.algebra.zmodp.html#Zp1"><span class="id" title="definition">Zp1</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_mulzV"><span class="id" title="lemma">Zp_mulzV</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#p"><span class="id" title="abbreviation">p</span></a> <a class="idref" href="mathcomp.algebra.zmodp.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#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_mul"><span class="id" title="definition">Zp_mul</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.algebra.zmodp.html#Zp_inv"><span class="id" title="definition">Zp_inv</span></a> <a class="idref" href="mathcomp.algebra.zmodp.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.algebra.zmodp.html#Zp1"><span class="id" title="definition">Zp1</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_intro_unit"><span class="id" title="lemma">Zp_intro_unit</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_mul"><span class="id" title="definition">Zp_mul</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.zmodp.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.algebra.zmodp.html#Zp1"><span class="id" title="definition">Zp1</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.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#p"><span class="id" title="abbreviation">p</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_inv_out"><span class="id" title="lemma">Zp_inv_out</span></a> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><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.algebra.zmodp.html#p"><span class="id" title="abbreviation">p</span></a> <a class="idref" href="mathcomp.algebra.zmodp.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#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_inv"><span class="id" title="definition">Zp_inv</span></a> <a class="idref" href="mathcomp.algebra.zmodp.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.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_mulrn"><span class="id" title="lemma">Zp_mulrn</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#e9001f602764f7896bb1eb34bf606a23"><span class="id" title="notation">*+</span></a> <a class="idref" href="mathcomp.algebra.zmodp.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.algebra.zmodp.html#inZp"><span class="id" title="definition">inZp</span></a> (<a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#n"><span class="id" title="variable">n</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_mulgC"><span class="id" title="lemma">Zp_mulgC</span></a> : @<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#commutative"><span class="id" title="definition">commutative</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#mulg"><span class="id" title="definition">mulg</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_abelian"><span class="id" title="lemma">Zp_abelian</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_expg"><span class="id" title="lemma">Zp_expg</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#06cdd2633d7788bac7abeac13b2dd91e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.algebra.zmodp.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.algebra.zmodp.html#inZp"><span class="id" title="definition">inZp</span></a> (<a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#n"><span class="id" title="variable">n</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp1_expgz"><span class="id" title="lemma">Zp1_expgz</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.zmodp.html#Zp1"><span class="id" title="definition">Zp1</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#06cdd2633d7788bac7abeac13b2dd91e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.algebra.zmodp.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.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_cycle"><span class="id" title="lemma">Zp_cycle</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#setT"><span class="id" title="abbreviation">setT</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.fingroup.fingroup.html#5e5825d099c952c2db2842c142cbde94"><span class="id" title="notation"><[</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#Zp1"><span class="id" title="definition">Zp1</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#5e5825d099c952c2db2842c142cbde94"><span class="id" title="notation">]></span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="order_Zp1"><span class="id" title="lemma">order_Zp1</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#09508509373ff3217fbbadb14d25dc5c"><span class="id" title="notation">#[</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#Zp1"><span class="id" title="definition">Zp1</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#09508509373ff3217fbbadb14d25dc5c"><span class="id" title="notation">]</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.zmodp.html#p"><span class="id" title="abbreviation">p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.zmodp.html#ZpDef"><span class="id" title="section">ZpDef</span></a>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="ord1"><span class="id" title="lemma">ord1</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#all_equal_to"><span class="id" title="definition">all_equal_to</span></a> (0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_1</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="lshift0"><span class="id" title="lemma">lshift0</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#lshift"><span class="id" title="definition">lshift</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#m"><span class="id" title="variable">m</span></a> (0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a>0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">).+1</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>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="rshift1"><span class="id" title="lemma">rshift1</span></a> <span class="id" title="var">n</span> : @<a class="idref" href="mathcomp.ssreflect.fintype.html#rshift"><span class="id" title="definition">rshift</span></a> 1 <a class="idref" href="mathcomp.algebra.zmodp.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.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#lift"><span class="id" title="definition">lift</span></a> (0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_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="split1"><span class="id" title="lemma">split1</span></a> <span class="id" title="var">n</span> <span class="id" title="var">i</span> :<br/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#split"><span class="id" title="definition">split</span></a> (<a class="idref" href="mathcomp.algebra.zmodp.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">(</span></a>1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">)</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#oapp"><span class="id" title="abbreviation">oapp</span></a> (@<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span>) (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <span class="id" title="var">_</span> 0) (<a class="idref" href="mathcomp.ssreflect.fintype.html#unlift"><span class="id" title="definition">unlift</span></a> 0 <a class="idref" href="mathcomp.algebra.zmodp.html#i"><span class="id" title="variable">i</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="big_ord1"><span class="id" title="lemma">big_ord1</span></a> <span class="id" title="var">R</span> <span class="id" title="var">idx</span> (<span class="id" title="var">op</span> : @<a class="idref" href="mathcomp.ssreflect.bigop.html#Monoid.law"><span class="id" title="record">Monoid.law</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#idx"><span class="id" title="variable">idx</span></a>) <span class="id" title="var">F</span> :<br/> - <a class="idref" href="mathcomp.ssreflect.bigop.html#afef6bddeda988bbc365e556241d5732"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#afef6bddeda988bbc365e556241d5732"><span class="id" title="notation">big</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#afef6bddeda988bbc365e556241d5732"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#op"><span class="id" title="variable">op</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#afef6bddeda988bbc365e556241d5732"><span class="id" title="notation">/</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#idx"><span class="id" title="variable">idx</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#afef6bddeda988bbc365e556241d5732"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#afef6bddeda988bbc365e556241d5732"><span class="id" title="notation">_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#afef6bddeda988bbc365e556241d5732"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#afef6bddeda988bbc365e556241d5732"><span class="id" title="notation"><</span></a> 1<a class="idref" href="mathcomp.ssreflect.bigop.html#afef6bddeda988bbc365e556241d5732"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#i"><span class="id" title="variable">i</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.zmodp.html#F"><span class="id" title="variable">F</span></a> 0.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="big_ord1_cond"><span class="id" title="lemma">big_ord1_cond</span></a> <span class="id" title="var">R</span> <span class="id" title="var">idx</span> (<span class="id" title="var">op</span> : @<a class="idref" href="mathcomp.ssreflect.bigop.html#Monoid.law"><span class="id" title="record">Monoid.law</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#idx"><span class="id" title="variable">idx</span></a>) <span class="id" title="var">P</span> <span class="id" title="var">F</span> :<br/> - <a class="idref" href="mathcomp.ssreflect.bigop.html#0b83d32979b1fdd5833879356bbfd57b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#0b83d32979b1fdd5833879356bbfd57b"><span class="id" title="notation">big</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#0b83d32979b1fdd5833879356bbfd57b"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#op"><span class="id" title="variable">op</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#0b83d32979b1fdd5833879356bbfd57b"><span class="id" title="notation">/</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#idx"><span class="id" title="variable">idx</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#0b83d32979b1fdd5833879356bbfd57b"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#0b83d32979b1fdd5833879356bbfd57b"><span class="id" title="notation">_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#0b83d32979b1fdd5833879356bbfd57b"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#0b83d32979b1fdd5833879356bbfd57b"><span class="id" title="notation"><</span></a> 1 <a class="idref" href="mathcomp.ssreflect.bigop.html#0b83d32979b1fdd5833879356bbfd57b"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#0b83d32979b1fdd5833879356bbfd57b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#i"><span class="id" title="variable">i</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#P"><span class="id" title="variable">P</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#F"><span class="id" title="variable">F</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#idx"><span class="id" title="variable">idx</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="ZpRing"><span class="id" title="section">ZpRing</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="ZpRing.p'"><span class="id" title="variable">p'</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>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_nontrivial"><span class="id" title="lemma">Zp_nontrivial</span></a> : <a class="idref" href="mathcomp.algebra.zmodp.html#Zp1"><span class="id" title="definition">Zp1</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.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a>. <br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Zp_ringMixin"><span class="id" title="definition">Zp_ringMixin</span></a> :=<br/> - <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ComRing.Exports.ComRingMixin"><span class="id" title="abbreviation">ComRingMixin</span></a> (@<a class="idref" href="mathcomp.algebra.zmodp.html#Zp_mulA"><span class="id" title="lemma">Zp_mulA</span></a> <span class="id" title="var">_</span>) (@<a class="idref" href="mathcomp.algebra.zmodp.html#Zp_mulC"><span class="id" title="lemma">Zp_mulC</span></a> <span class="id" title="var">_</span>) (@<a class="idref" href="mathcomp.algebra.zmodp.html#Zp_mul1z"><span class="id" title="lemma">Zp_mul1z</span></a> <span class="id" title="var">_</span>) (@<a class="idref" href="mathcomp.algebra.zmodp.html#Zp_mul_addl"><span class="id" title="lemma">Zp_mul_addl</span></a> <span class="id" title="var">_</span>)<br/> - <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_nontrivial"><span class="id" title="lemma">Zp_nontrivial</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_ringType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.RingType"><span class="id" title="abbreviation">RingType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_ringMixin"><span class="id" title="definition">Zp_ringMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_finRingType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11"><span class="id" title="notation">finRingType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a><a class="idref" href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_comRingType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ComRing.Exports.ComRingType"><span class="id" title="abbreviation">ComRingType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a> (@<a class="idref" href="mathcomp.algebra.zmodp.html#Zp_mulC"><span class="id" title="lemma">Zp_mulC</span></a> <span class="id" title="var">_</span>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_finComRingType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.finalg.html#b13c97e55bebdc1c181a99b80106c099"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#b13c97e55bebdc1c181a99b80106c099"><span class="id" title="notation">finComRingType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#b13c97e55bebdc1c181a99b80106c099"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a><a class="idref" href="mathcomp.algebra.finalg.html#b13c97e55bebdc1c181a99b80106c099"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Zp_unitRingMixin"><span class="id" title="definition">Zp_unitRingMixin</span></a> :=<br/> - <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ComUnitRing.Exports.ComUnitRingMixin"><span class="id" title="abbreviation">ComUnitRingMixin</span></a> (@<a class="idref" href="mathcomp.algebra.zmodp.html#Zp_mulVz"><span class="id" title="lemma">Zp_mulVz</span></a> <span class="id" title="var">_</span>) (@<a class="idref" href="mathcomp.algebra.zmodp.html#Zp_intro_unit"><span class="id" title="lemma">Zp_intro_unit</span></a> <span class="id" title="var">_</span>) (@<a class="idref" href="mathcomp.algebra.zmodp.html#Zp_inv_out"><span class="id" title="lemma">Zp_inv_out</span></a> <span class="id" title="var">_</span>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_unitRingType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.UnitRing.Exports.UnitRingType"><span class="id" title="abbreviation">UnitRingType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_unitRingMixin"><span class="id" title="definition">Zp_unitRingMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_finUnitRingType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.finalg.html#157b0761db3726d8e1bc0a71108dc48f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#157b0761db3726d8e1bc0a71108dc48f"><span class="id" title="notation">finUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#157b0761db3726d8e1bc0a71108dc48f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a><a class="idref" href="mathcomp.algebra.finalg.html#157b0761db3726d8e1bc0a71108dc48f"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_comUnitRingType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">comUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_finComUnitRingType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.finalg.html#29c2dac4b2cace3201f3f23b551d143a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#29c2dac4b2cace3201f3f23b551d143a"><span class="id" title="notation">finComUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#29c2dac4b2cace3201f3f23b551d143a"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a><a class="idref" href="mathcomp.algebra.finalg.html#29c2dac4b2cace3201f3f23b551d143a"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_nat"><span class="id" title="lemma">Zp_nat</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.algebra.zmodp.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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#inZp"><span class="id" title="definition">inZp</span></a> <a class="idref" href="mathcomp.algebra.zmodp.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#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="natr_Zp"><span class="id" title="lemma">natr_Zp</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a>) : <a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</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="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.zmodp.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="natr_negZp"><span class="id" title="lemma">natr_negZp</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</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#8d0566c961139ec21811f52ef0c317db"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</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="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#8d0566c961139ec21811f52ef0c317db"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="unit_Zp_mulgC"><span class="id" title="lemma">unit_Zp_mulgC</span></a> : @<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#commutative"><span class="id" title="definition">commutative</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#18d0918a160c839bc9f32d8e64dd406d"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.finalg.html#18d0918a160c839bc9f32d8e64dd406d"><span class="id" title="notation">unit</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a><a class="idref" href="mathcomp.algebra.finalg.html#18d0918a160c839bc9f32d8e64dd406d"><span class="id" title="notation">}</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#mulg"><span class="id" title="definition">mulg</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="unit_Zp_expg"><span class="id" title="lemma">unit_Zp_expg</span></a> (<span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.finalg.html#18d0918a160c839bc9f32d8e64dd406d"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.finalg.html#18d0918a160c839bc9f32d8e64dd406d"><span class="id" title="notation">unit</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a><a class="idref" href="mathcomp.algebra.finalg.html#18d0918a160c839bc9f32d8e64dd406d"><span class="id" title="notation">}</span></a>) <span class="id" title="var">n</span> :<br/> - <a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> (<a class="idref" href="mathcomp.algebra.zmodp.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#06cdd2633d7788bac7abeac13b2dd91e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.algebra.zmodp.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#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#inZp"><span class="id" title="definition">inZp</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.zmodp.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#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.zmodp.html#ZpRing"><span class="id" title="section">ZpRing</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Zp_trunc"><span class="id" title="definition">Zp_trunc</span></a> <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.algebra.zmodp.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#b9f3db5365f11e72cad3907646ac5a3a"><span class="id" title="notation">.-2</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">"</span></a>''Z_' p" := <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bc63483175fac06bcd5541a5e9093b18"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#Zp_trunc"><span class="id" title="definition">Zp_trunc</span></a> <span class="id" title="var">p</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bc63483175fac06bcd5541a5e9093b18"><span class="id" title="notation">).+2</span></a><br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">p</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "''Z_' p") : <span class="id" title="var">type_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">"</span></a>''F_' p" := <a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">Z_</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#pdiv"><span class="id" title="definition">pdiv</span></a> <span class="id" title="var">p</span><a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">)</span></a><br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">p</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "''F_' p") : <span class="id" title="var">type_scope</span>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Groups"><span class="id" title="section">Groups</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="Groups.p"><span class="id" title="variable">p</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>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Zp"><span class="id" title="definition">Zp</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Groups.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#7f2a7ef2c63af7359b22787a9daf336e"><span class="id" title="notation">></span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">Z_p</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">else</span></a> 1%<span class="id" title="var">g</span>.<br/> -<span class="id" title="keyword">Definition</span> <a name="units_Zp"><span class="id" title="definition">units_Zp</span></a> := <a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#18d0918a160c839bc9f32d8e64dd406d"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.finalg.html#18d0918a160c839bc9f32d8e64dd406d"><span class="id" title="notation">unit</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">Z_p</span></a><a class="idref" href="mathcomp.algebra.finalg.html#18d0918a160c839bc9f32d8e64dd406d"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_cast"><span class="id" title="lemma">Zp_cast</span></a> : <a class="idref" href="mathcomp.algebra.zmodp.html#Groups.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#7f2a7ef2c63af7359b22787a9daf336e"><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#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#bc63483175fac06bcd5541a5e9093b18"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#Zp_trunc"><span class="id" title="definition">Zp_trunc</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Groups.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bc63483175fac06bcd5541a5e9093b18"><span class="id" title="notation">).+2</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.zmodp.html#Groups.p"><span class="id" title="variable">p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="val_Zp_nat"><span class="id" title="lemma">val_Zp_nat</span></a> (<span class="id" title="var">p_gt1</span> : <a class="idref" href="mathcomp.algebra.zmodp.html#Groups.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#7f2a7ef2c63af7359b22787a9daf336e"><span class="id" title="notation">></span></a> 1) <span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.zmodp.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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">Z_p</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.algebra.zmodp.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#e3d79e08e7e529cc9ef532e000103386"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Groups.p"><span class="id" title="variable">p</span></a>)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></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>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_nat_mod"><span class="id" title="lemma">Zp_nat_mod</span></a> (<span class="id" title="var">p_gt1</span> : <a class="idref" href="mathcomp.algebra.zmodp.html#Groups.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#7f2a7ef2c63af7359b22787a9daf336e"><span class="id" title="notation">></span></a> 1)<span class="id" title="var">m</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#e3d79e08e7e529cc9ef532e000103386"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Groups.p"><span class="id" title="variable">p</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#m"><span class="id" title="variable">m</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">Z_p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="char_Zp"><span class="id" title="lemma">char_Zp</span></a> : <a class="idref" href="mathcomp.algebra.zmodp.html#Groups.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#7f2a7ef2c63af7359b22787a9daf336e"><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#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Groups.p"><span class="id" title="variable">p</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">Z_p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="unitZpE"><span class="id" title="lemma">unitZpE</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.zmodp.html#Groups.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#7f2a7ef2c63af7359b22787a9daf336e"><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#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">Z_p</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">a</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.unit"><span class="id" title="definition">GRing.unit</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="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.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Groups.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Zp_group_set"><span class="id" title="lemma">Zp_group_set</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#group_set"><span class="id" title="definition">group_set</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp"><span class="id" title="definition">Zp</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_group</span> := <a class="idref" href="mathcomp.fingroup.fingroup.html#Group"><span class="id" title="constructor">Group</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp_group_set"><span class="id" title="lemma">Zp_group_set</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="card_Zp"><span class="id" title="lemma">card_Zp</span></a> : <a class="idref" href="mathcomp.algebra.zmodp.html#Groups.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#7f2a7ef2c63af7359b22787a9daf336e"><span class="id" title="notation">></span></a> 0 <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.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#Zp"><span class="id" title="definition">Zp</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</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.zmodp.html#Groups.p"><span class="id" title="variable">p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="mem_Zp"><span class="id" title="lemma">mem_Zp</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.zmodp.html#Groups.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#7f2a7ef2c63af7359b22787a9daf336e"><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#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Zp"><span class="id" title="definition">Zp</span></a>. <br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">units_Zp_group</span> := <a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#units_Zp"><span class="id" title="definition">units_Zp</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="card_units_Zp"><span class="id" title="lemma">card_units_Zp</span></a> : <a class="idref" href="mathcomp.algebra.zmodp.html#Groups.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#7f2a7ef2c63af7359b22787a9daf336e"><span class="id" title="notation">></span></a> 0 <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.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#units_Zp"><span class="id" title="definition">units_Zp</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</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.prime.html#totient"><span class="id" title="definition">totient</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Groups.p"><span class="id" title="variable">p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="units_Zp_abelian"><span class="id" title="lemma">units_Zp_abelian</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#units_Zp"><span class="id" title="definition">units_Zp</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.zmodp.html#Groups"><span class="id" title="section">Groups</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - Field structure for primes. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Section</span> <a name="PrimeField"><span class="id" title="section">PrimeField</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">ring_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="PrimeField.p"><span class="id" title="variable">p</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>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="PrimeField.F_prime"><span class="id" title="section">F_prime</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Hypothesis</span> <a name="PrimeField.F_prime.p_pr"><span class="id" title="variable">p_pr</span></a> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#PrimeField.p"><span class="id" title="variable">p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Fp_Zcast"><span class="id" title="lemma">Fp_Zcast</span></a> : <a class="idref" href="mathcomp.ssreflect.ssrnat.html#bc63483175fac06bcd5541a5e9093b18"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#Zp_trunc"><span class="id" title="definition">Zp_trunc</span></a> (<a class="idref" href="mathcomp.ssreflect.prime.html#pdiv"><span class="id" title="definition">pdiv</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#PrimeField.p"><span class="id" title="variable">p</span></a>)<a class="idref" href="mathcomp.ssreflect.ssrnat.html#bc63483175fac06bcd5541a5e9093b18"><span class="id" title="notation">).+2</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#bc63483175fac06bcd5541a5e9093b18"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#Zp_trunc"><span class="id" title="definition">Zp_trunc</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#PrimeField.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bc63483175fac06bcd5541a5e9093b18"><span class="id" title="notation">).+2</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Fp_cast"><span class="id" title="lemma">Fp_cast</span></a> : <a class="idref" href="mathcomp.ssreflect.ssrnat.html#bc63483175fac06bcd5541a5e9093b18"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#Zp_trunc"><span class="id" title="definition">Zp_trunc</span></a> (<a class="idref" href="mathcomp.ssreflect.prime.html#pdiv"><span class="id" title="definition">pdiv</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#PrimeField.p"><span class="id" title="variable">p</span></a>)<a class="idref" href="mathcomp.ssreflect.ssrnat.html#bc63483175fac06bcd5541a5e9093b18"><span class="id" title="notation">).+2</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.zmodp.html#PrimeField.p"><span class="id" title="variable">p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="card_Fp"><span class="id" title="lemma">card_Fp</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</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.zmodp.html#PrimeField.p"><span class="id" title="variable">p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="val_Fp_nat"><span class="id" title="lemma">val_Fp_nat</span></a> <span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.zmodp.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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.algebra.zmodp.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#e3d79e08e7e529cc9ef532e000103386"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#PrimeField.p"><span class="id" title="variable">p</span></a>)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></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>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Fp_nat_mod"><span class="id" title="lemma">Fp_nat_mod</span></a> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#e3d79e08e7e529cc9ef532e000103386"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#PrimeField.p"><span class="id" title="variable">p</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#m"><span class="id" title="variable">m</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="char_Fp"><span class="id" title="lemma">char_Fp</span></a> : <a class="idref" href="mathcomp.algebra.zmodp.html#PrimeField.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="char_Fp_0"><span class="id" title="lemma">char_Fp_0</span></a> : <a class="idref" href="mathcomp.algebra.zmodp.html#PrimeField.p"><span class="id" title="variable">p</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="unitFpE"><span class="id" title="lemma">unitFpE</span></a> <span class="id" title="var">x</span> : <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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">a</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.unit"><span class="id" title="definition">GRing.unit</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="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.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#PrimeField.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.zmodp.html#PrimeField.F_prime"><span class="id" title="section">F_prime</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Fp_fieldMixin"><span class="id" title="lemma">Fp_fieldMixin</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.mixin_of"><span class="id" title="definition">GRing.Field.mixin_of</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#dd4e793ea9d0dbe0a320346aa74c809d"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#dd4e793ea9d0dbe0a320346aa74c809d"><span class="id" title="notation">the</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.UnitRing.Exports.unitRingType"><span class="id" title="abbreviation">unitRingType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#dd4e793ea9d0dbe0a320346aa74c809d"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#dd4e793ea9d0dbe0a320346aa74c809d"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Fp_idomainMixin"><span class="id" title="definition">Fp_idomainMixin</span></a> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.FieldIdomainMixin"><span class="id" title="abbreviation">FieldIdomainMixin</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Fp_fieldMixin"><span class="id" title="lemma">Fp_fieldMixin</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Fp_idomainType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.Exports.IdomainType"><span class="id" title="abbreviation">IdomainType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Fp_idomainMixin"><span class="id" title="definition">Fp_idomainMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Fp_finIdomainType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.finalg.html#762465ada9848b70124d860dd97a755c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#762465ada9848b70124d860dd97a755c"><span class="id" title="notation">finIdomainType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#762465ada9848b70124d860dd97a755c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a><a class="idref" href="mathcomp.algebra.finalg.html#762465ada9848b70124d860dd97a755c"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Fp_fieldType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.FieldType"><span class="id" title="abbreviation">FieldType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Fp_fieldMixin"><span class="id" title="lemma">Fp_fieldMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Fp_finFieldType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.finalg.html#85a9f33cca8b2a31e30517c43d5ecb47"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#85a9f33cca8b2a31e30517c43d5ecb47"><span class="id" title="notation">finFieldType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#85a9f33cca8b2a31e30517c43d5ecb47"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a><a class="idref" href="mathcomp.algebra.finalg.html#85a9f33cca8b2a31e30517c43d5ecb47"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Fp_decFieldType</span> :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#29a9c5427a3ebd772d1548a40a20219d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#29a9c5427a3ebd772d1548a40a20219d"><span class="id" title="notation">decFieldType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#29a9c5427a3ebd772d1548a40a20219d"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#29a9c5427a3ebd772d1548a40a20219d"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#Fp_finFieldType"><span class="id" title="definition">Fp_finFieldType</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#29a9c5427a3ebd772d1548a40a20219d"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.zmodp.html#PrimeField"><span class="id" title="section">PrimeField</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_countZmodType</span> <span class="id" title="var">m</span> := <a class="idref" href="mathcomp.algebra.countalg.html#c4cf911b6276243d26c2dd85fdb53f8f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.countalg.html#c4cf911b6276243d26c2dd85fdb53f8f"><span class="id" title="notation">countZmodType</span></a> <a class="idref" href="mathcomp.algebra.countalg.html#c4cf911b6276243d26c2dd85fdb53f8f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.algebra.countalg.html#c4cf911b6276243d26c2dd85fdb53f8f"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_countRingType</span> <span class="id" title="var">m</span> := <a class="idref" href="mathcomp.algebra.countalg.html#5d38f59e59d31b0f5328b7330ff4d0f6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.countalg.html#5d38f59e59d31b0f5328b7330ff4d0f6"><span class="id" title="notation">countRingType</span></a> <a class="idref" href="mathcomp.algebra.countalg.html#5d38f59e59d31b0f5328b7330ff4d0f6"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bc63483175fac06bcd5541a5e9093b18"><span class="id" title="notation">.+2</span></a><a class="idref" href="mathcomp.algebra.countalg.html#5d38f59e59d31b0f5328b7330ff4d0f6"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_countComRingType</span> <span class="id" title="var">m</span> := <a class="idref" href="mathcomp.algebra.countalg.html#d271043791f97708a05788e885686caa"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.countalg.html#d271043791f97708a05788e885686caa"><span class="id" title="notation">countComRingType</span></a> <a class="idref" href="mathcomp.algebra.countalg.html#d271043791f97708a05788e885686caa"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bc63483175fac06bcd5541a5e9093b18"><span class="id" title="notation">.+2</span></a><a class="idref" href="mathcomp.algebra.countalg.html#d271043791f97708a05788e885686caa"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_countUnitRingType</span> <span class="id" title="var">m</span> := <a class="idref" href="mathcomp.algebra.countalg.html#d7279d52944865f8d2b1e61af96c64e0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.countalg.html#d7279d52944865f8d2b1e61af96c64e0"><span class="id" title="notation">countUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.countalg.html#d7279d52944865f8d2b1e61af96c64e0"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bc63483175fac06bcd5541a5e9093b18"><span class="id" title="notation">.+2</span></a><a class="idref" href="mathcomp.algebra.countalg.html#d7279d52944865f8d2b1e61af96c64e0"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Zp_countComUnitRingType</span> <span class="id" title="var">m</span> := <a class="idref" href="mathcomp.algebra.countalg.html#6e623071866dc1a29a10d36cc1dfa886"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.countalg.html#6e623071866dc1a29a10d36cc1dfa886"><span class="id" title="notation">countComUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.countalg.html#6e623071866dc1a29a10d36cc1dfa886"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bc63483175fac06bcd5541a5e9093b18"><span class="id" title="notation">.+2</span></a><a class="idref" href="mathcomp.algebra.countalg.html#6e623071866dc1a29a10d36cc1dfa886"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Fp_countIdomainType</span> <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.algebra.countalg.html#deee2c5961371227bcb71bc712dbd08f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.countalg.html#deee2c5961371227bcb71bc712dbd08f"><span class="id" title="notation">countIdomainType</span></a> <a class="idref" href="mathcomp.algebra.countalg.html#deee2c5961371227bcb71bc712dbd08f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a><a class="idref" href="mathcomp.algebra.countalg.html#deee2c5961371227bcb71bc712dbd08f"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Fp_countFieldType</span> <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.algebra.countalg.html#7ca0985aed2b28afaaa4007eb0a80f3a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.countalg.html#7ca0985aed2b28afaaa4007eb0a80f3a"><span class="id" title="notation">countFieldType</span></a> <a class="idref" href="mathcomp.algebra.countalg.html#7ca0985aed2b28afaaa4007eb0a80f3a"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a><a class="idref" href="mathcomp.algebra.countalg.html#7ca0985aed2b28afaaa4007eb0a80f3a"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Fp_countDecFieldType</span> <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.algebra.countalg.html#1ab55886e2b992f0c2d8591f02a7baf7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.countalg.html#1ab55886e2b992f0c2d8591f02a7baf7"><span class="id" title="notation">countDecFieldType</span></a> <a class="idref" href="mathcomp.algebra.countalg.html#1ab55886e2b992f0c2d8591f02a7baf7"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a><a class="idref" href="mathcomp.algebra.countalg.html#1ab55886e2b992f0c2d8591f02a7baf7"><span class="id" title="notation">]</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 |