generate the documentation for 1.7

author: Enrico Tassi 2018-04-20 10:54:22 +0200
committer: Enrico Tassi 2018-04-20 10:54:22 +0200
commit: ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch)
tree: e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.field.finfield.html
parent: 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)
1 files changed, 510 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.field.finfield.html b/docs/htmldoc/mathcomp.field.finfield.html
new file mode 100644
index 0000000..c6454db
--- /dev/null
+++ b/docs/htmldoc/mathcomp.field.finfield.html
@@ -0,0 +1,510 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
+<link href="coqdoc.css" rel="stylesheet" type="text/css" />
+<title>mathcomp.field.finfield</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library mathcomp.field.finfield</h1>
+
+<div class="code">
+<span class="comment">(*&nbsp;(c)&nbsp;Copyright&nbsp;2006-2016&nbsp;Microsoft&nbsp;Corporation&nbsp;and&nbsp;Inria.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
+&nbsp;Distributed&nbsp;under&nbsp;the&nbsp;terms&nbsp;of&nbsp;CeCILL-B.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+  Additional constructions and results on finite fields.                    
+
+<div class="paragraph"> </div>
+
+         FinFieldExtType L == A FinFieldType structure on the carrier of L, 
+                              where L IS a fieldExtType F structure for an  
+                              F that has a finFieldType structure. This     
+                              does not take any existing finType structure  
+                              on L; this should not be made canonical.      
+ FinSplittingFieldType F L == A SplittingFieldType F structure on the       
+                              carrier of L, where L IS a fieldExtType F for 
+                              an F with a finFieldType structure; this      
+                              should not be made canonical.                 
+          Import FinVector :: Declares canonical default finType, finRing,  
+                              etc structures (including FinFieldExtType     
+                              above) for abstract vectType, FalgType and    
+                              fieldExtType over a finFieldType. This should 
+                              be used with caution (e.g., local to a proof) 
+                              as the finType so obtained may clash with the 
+                              canonical one for standard types like matrix. 
+      PrimeCharType charRp == The carrier of a ringType R such that         
+                              charRp : p \in [char R] holds. This type has  
+                              canonical ringType, ..., fieldType structures 
+                              compatible with those of R, as well as        
+                              canonical lmodType 'F_p, ..., algType 'F_p    
+                              structures, plus an FalgType structure if R   
+                              is a finUnitRingType and a splittingFieldType 
+                              struture if R is a finFieldType.              
+ FinSplittingFieldFor nz_p == sigma-pair whose sval is a splittingFieldType 
+                              that is the splitting field for p : {poly F}  
+                              over F : finFieldType, given nz_p : p != 0.   
+ PrimePowerField pr_p k_gt0 == sigma2-triple whose s2val is a finFieldType  
+                              of characteristic p and order m = p ^ k,      
+                              given pr_p : prime p and k_gt0 : k &gt; 0.       
+   FinDomainFieldType domR == A finFieldType structure on a finUnitRingType 
+                              R, given domR : GRing.IntegralDomain.axiom R. 
+                              This is intended to be used inside proofs,    
+                              where one cannot declare Canonical instances. 
+                              Otherwise one should construct explicitly the 
+                              intermediate structures using the ssralg and  
+                              finalg constructors, and finDomain_mulrC domR 
+                              finDomain_fieldP domR to prove commutativity  
+                              and field axioms (the former is Wedderburn's  
+                              little theorem).                              
+ FinDomainSplittingFieldType domR charRp == A splittingFieldType structure  
+                              that repackages the two constructions above.   
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span> <span class="id" title="var">GRing.Theory</span> <span class="id" title="var">FinRing.Theory</span>.<br/>
+<span class="id" title="keyword">Local Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">ring_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="FinRing"><span class="id" title="section">FinRing</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="FinRing.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Ring.Exports.finRingType"><span class="id" title="abbreviation">finRingType</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="finRing_nontrivial"><span class="id" title="lemma">finRing_nontrivial</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinRing.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 1%<span class="id" title="var">g</span>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="finRing_gt1"><span class="id" title="lemma">finRing_gt1</span></a> : 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.field.finfield.html#FinRing.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#FinRing"><span class="id" title="section">FinRing</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="FinField"><span class="id" title="section">FinField</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="FinField.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Field.Exports.finFieldType"><span class="id" title="abbreviation">finFieldType</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_finField_unit"><span class="id" title="lemma">card_finField_unit</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#f7c6b2be51cd10aae4ae8951352903f1"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.finalg.html#f7c6b2be51cd10aae4ae8951352903f1"><span class="id" title="notation">unit</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.finalg.html#f7c6b2be51cd10aae4ae8951352903f1"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="finField_unit"><span class="id" title="definition">finField_unit</span></a> <span class="id" title="var">x</span> (<span class="id" title="var">nz_x</span> : <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0) :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.finalg.html#FinRing.unit"><span class="id" title="abbreviation">FinRing.unit</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#etrans"><span class="id" title="definition">etrans</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Theory.unitfE"><span class="id" title="definition">unitfE</span></a> <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.field.finfield.html#nz_x"><span class="id" title="variable">nz_x</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="expf_card"><span class="id" title="lemma">expf_card</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="finField_genPoly"><span class="id" title="lemma">finField_genPoly</span></a> : <a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d70623330b2787db6b196e37db7d8f45"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">X</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#24846b5795605f82696a43aa191874ea"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#24846b5795605f82696a43aa191874ea"><span class="id" title="notation">prod_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#24846b5795605f82696a43aa191874ea"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">X</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d70623330b2787db6b196e37db7d8f45"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#24846b5795605f82696a43aa191874ea"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="finCharP"><span class="id" title="lemma">finCharP</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">{</span></a><span class="id" title="var">p</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.field.finfield.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.field.finfield.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="finField_is_abelem"><span class="id" title="lemma">finField_is_abelem</span></a> : <a class="idref" href="mathcomp.solvable.abelian.html#is_abelem"><span class="id" title="definition">is_abelem</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_finCharP"><span class="id" title="lemma">card_finCharP</span></a> <span class="id" title="var">p</span> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.field.finfield.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.field.finfield.html#n"><span class="id" title="variable">n</span></a>)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.field.finfield.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.finfield.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#FinField"><span class="id" title="section">FinField</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="CardVspace"><span class="id" title="section">CardVspace</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="CardVspace.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Field.Exports.finFieldType"><span class="id" title="abbreviation">finFieldType</span></a>) (<a name="CardVspace.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="CardVspace.Vector"><span class="id" title="section">Vector</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="CardVspace.Vector.cvT"><span class="id" title="variable">cvT</span></a> : <a class="idref" href="mathcomp.algebra.vector.html#Vector.class_of"><span class="id" title="record">Vector.class_of</span></a> <a class="idref" href="mathcomp.field.finfield.html#CardVspace.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.field.finfield.html#CardVspace.T"><span class="id" title="variable">T</span></a>.<br/>
+<span class="id" title="keyword">Let</span> <a name="CardVspace.Vector.vT"><span class="id" title="variable">vT</span></a> := <a class="idref" href="mathcomp.algebra.vector.html#Vector.Pack"><span class="id" title="constructor">Vector.Pack</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <a class="idref" href="mathcomp.field.finfield.html#CardVspace.F"><span class="id" title="variable">F</span></a>) <a class="idref" href="mathcomp.field.finfield.html#CardVspace.Vector.cvT"><span class="id" title="variable">cvT</span></a> <a class="idref" href="mathcomp.field.finfield.html#CardVspace.T"><span class="id" title="variable">T</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_vspace"><span class="id" title="lemma">card_vspace</span></a> (<span class="id" title="var">V</span> : <a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">vspace</span></a> <a class="idref" href="mathcomp.field.finfield.html#CardVspace.Vector.vT"><span class="id" title="variable">vT</span></a><a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.field.finfield.html#V"><span class="id" title="variable">V</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.field.finfield.html#CardVspace.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.vector.html#ee35a6780ccd60155a3be89dcb5fdb30"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.vector.html#ee35a6780ccd60155a3be89dcb5fdb30"><span class="id" title="notation">dim</span></a> <a class="idref" href="mathcomp.field.finfield.html#V"><span class="id" title="variable">V</span></a>)%<span class="id" title="var">N</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_vspacef"><span class="id" title="lemma">card_vspacef</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.algebra.vector.html#899a5fd19c4f3564d9757a9ac446b1dc"><span class="id" title="notation">{:</span></a> <a class="idref" href="mathcomp.field.finfield.html#CardVspace.Vector.vT"><span class="id" title="variable">vT</span></a><a class="idref" href="mathcomp.algebra.vector.html#899a5fd19c4f3564d9757a9ac446b1dc"><span class="id" title="notation">}</span></a>%<span class="id" title="var">VS</span><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.field.finfield.html#CardVspace.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#CardVspace.Vector"><span class="id" title="section">Vector</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="CardVspace.caT"><span class="id" title="variable">caT</span></a> : <a class="idref" href="mathcomp.field.falgebra.html#Falgebra.class_of"><span class="id" title="record">Falgebra.class_of</span></a> <a class="idref" href="mathcomp.field.finfield.html#CardVspace.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.field.finfield.html#CardVspace.T"><span class="id" title="variable">T</span></a>.<br/>
+<span class="id" title="keyword">Let</span> <a name="CardVspace.aT"><span class="id" title="variable">aT</span></a> := <a class="idref" href="mathcomp.field.falgebra.html#Falgebra.Pack"><span class="id" title="constructor">Falgebra.Pack</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <a class="idref" href="mathcomp.field.finfield.html#CardVspace.F"><span class="id" title="variable">F</span></a>) <a class="idref" href="mathcomp.field.finfield.html#CardVspace.caT"><span class="id" title="variable">caT</span></a> <a class="idref" href="mathcomp.field.finfield.html#CardVspace.T"><span class="id" title="variable">T</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_vspace1"><span class="id" title="lemma">card_vspace1</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|(</span></a>1%<span class="id" title="var">VS</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">vspace</span></a> <a class="idref" href="mathcomp.field.finfield.html#CardVspace.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">)|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.field.finfield.html#CardVspace.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#CardVspace"><span class="id" title="section">CardVspace</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="VectFinMixin"><span class="id" title="lemma">VectFinMixin</span></a> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Ring.Exports.finRingType"><span class="id" title="abbreviation">finRingType</span></a>) (<span class="id" title="var">vT</span> : <a class="idref" href="mathcomp.algebra.vector.html#Vector.Exports.vectType"><span class="id" title="abbreviation">vectType</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="variable">R</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.mixin_of"><span class="id" title="record">Finite.mixin_of</span></a> <a class="idref" href="mathcomp.field.finfield.html#vT"><span class="id" title="variable">vT</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ These instancces are not exported by default because they conflict with    
+ existing finType instances such as matrix_finType or primeChar_finType.     
+</div>
+<div class="code">
+<span class="id" title="keyword">Module</span> <a name="FinVector"><span class="id" title="module">FinVector</span></a>.<br/>
+<span class="id" title="keyword">Section</span> <a name="FinVector.Interfaces"><span class="id" title="section">Interfaces</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="FinVector.Interfaces.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Field.Exports.finFieldType"><span class="id" title="abbreviation">finFieldType</span></a>.<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">vT</span> : <a class="idref" href="mathcomp.algebra.vector.html#Vector.Exports.vectType"><span class="id" title="abbreviation">vectType</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinVector.Interfaces.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">aT</span> : <a class="idref" href="mathcomp.field.falgebra.html#Falgebra.Exports.FalgType"><span class="id" title="abbreviation">FalgType</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinVector.Interfaces.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">fT</span> : <a class="idref" href="mathcomp.field.fieldext.html#FieldExt.Exports.fieldExtType"><span class="id" title="abbreviation">fieldExtType</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinVector.Interfaces.F"><span class="id" title="variable">F</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">vect_finType</span> <span class="id" title="var">vT</span> := <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinType"><span class="id" title="abbreviation">FinType</span></a> <a class="idref" href="mathcomp.field.finfield.html#vT"><span class="id" title="variable">vT</span></a> (<a class="idref" href="mathcomp.field.finfield.html#VectFinMixin"><span class="id" title="lemma">VectFinMixin</span></a> <a class="idref" href="mathcomp.field.finfield.html#vT"><span class="id" title="variable">vT</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Falg_finType</span> <span class="id" title="var">aT</span> := <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinType"><span class="id" title="abbreviation">FinType</span></a> <a class="idref" href="mathcomp.field.finfield.html#aT"><span class="id" title="variable">aT</span></a> (<a class="idref" href="mathcomp.field.finfield.html#VectFinMixin"><span class="id" title="lemma">VectFinMixin</span></a> <a class="idref" href="mathcomp.field.finfield.html#aT"><span class="id" title="variable">aT</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fieldExt_finType</span> <span class="id" title="var">fT</span> := <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinType"><span class="id" title="abbreviation">FinType</span></a> <a class="idref" href="mathcomp.field.finfield.html#fT"><span class="id" title="variable">fT</span></a> (<a class="idref" href="mathcomp.field.finfield.html#VectFinMixin"><span class="id" title="lemma">VectFinMixin</span></a> <a class="idref" href="mathcomp.field.finfield.html#fT"><span class="id" title="variable">fT</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Falg_finRingType</span> <span class="id" title="var">aT</span> := <a class="idref" href="mathcomp.algebra.finalg.html#cf58bd711195f609ec57107fc402496c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#cf58bd711195f609ec57107fc402496c"><span class="id" title="notation">finRingType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#cf58bd711195f609ec57107fc402496c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.algebra.finalg.html#cf58bd711195f609ec57107fc402496c"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fieldExt_finRingType</span> <span class="id" title="var">fT</span> := <a class="idref" href="mathcomp.algebra.finalg.html#cf58bd711195f609ec57107fc402496c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#cf58bd711195f609ec57107fc402496c"><span class="id" title="notation">finRingType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#cf58bd711195f609ec57107fc402496c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#fT"><span class="id" title="variable">fT</span></a><a class="idref" href="mathcomp.algebra.finalg.html#cf58bd711195f609ec57107fc402496c"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fieldExt_finFieldType</span> <span class="id" title="var">fT</span> := <a class="idref" href="mathcomp.algebra.finalg.html#07fdfbae2c02044f4dae6b5dbeb0c7c7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#07fdfbae2c02044f4dae6b5dbeb0c7c7"><span class="id" title="notation">finFieldType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#07fdfbae2c02044f4dae6b5dbeb0c7c7"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#fT"><span class="id" title="variable">fT</span></a><a class="idref" href="mathcomp.algebra.finalg.html#07fdfbae2c02044f4dae6b5dbeb0c7c7"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FinVector.finField_splittingField_axiom"><span class="id" title="lemma">finField_splittingField_axiom</span></a> <span class="id" title="var">fT</span> : <a class="idref" href="mathcomp.field.galois.html#SplittingField.axiom"><span class="id" title="definition">SplittingField.axiom</span></a> <a class="idref" href="mathcomp.field.finfield.html#fT"><span class="id" title="variable">fT</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#FinVector.Interfaces"><span class="id" title="section">Interfaces</span></a>.<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#FinVector"><span class="id" title="module">FinVector</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="FinFieldExtType"><span class="id" title="abbreviation">FinFieldExtType</span></a> := <a class="idref" href="mathcomp.field.finfield.html#fieldExt_finFieldType"><span class="id" title="definition">FinVector.fieldExt_finFieldType</span></a>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="FinSplittingFieldAxiom"><span class="id" title="abbreviation">FinSplittingFieldAxiom</span></a> := (<a class="idref" href="mathcomp.field.finfield.html#finField_splittingField_axiom"><span class="id" title="lemma">FinVector.finField_splittingField_axiom</span></a> <span class="id" title="var">_</span>).<br/>
+<span class="id" title="keyword">Notation</span> <a name="FinSplittingFieldType"><span class="id" title="abbreviation">FinSplittingFieldType</span></a> <span class="id" title="var">F</span> <span class="id" title="var">L</span> :=<br/>
+&nbsp;&nbsp;(<a class="idref" href="mathcomp.field.galois.html#SplittingField.Exports.SplittingFieldType"><span class="id" title="abbreviation">SplittingFieldType</span></a> <span class="id" title="var">F</span> <span class="id" title="var">L</span> <a class="idref" href="mathcomp.field.finfield.html#FinSplittingFieldAxiom"><span class="id" title="abbreviation">FinSplittingFieldAxiom</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="PrimeChar"><span class="id" title="section">PrimeChar</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="PrimeChar.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="PrimeChar.PrimeCharRing"><span class="id" title="section">PrimeCharRing</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="PrimeChar.PrimeCharRing.R0"><span class="id" title="variable">R0</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="PrimeCharType"><span class="id" title="definition">PrimeCharType</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.PrimeCharRing.R0"><span class="id" title="variable">R0</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">]</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predArgType"><span class="id" title="definition">predArgType</span></a> := <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.PrimeCharRing.R0"><span class="id" title="variable">R0</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Hypothesis</span> <a name="PrimeChar.PrimeCharRing.charRp"><span class="id" title="variable">charRp</span></a> : <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.PrimeCharRing.R0"><span class="id" title="variable">R0</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">a</span> <span class="id" title="var">b</span> : <a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">F_p</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_eqType</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_choiceType</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_zmodType</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#af6385fc2df84aeeec6855073f75cc68"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af6385fc2df84aeeec6855073f75cc68"><span class="id" title="notation">zmodType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#af6385fc2df84aeeec6855073f75cc68"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af6385fc2df84aeeec6855073f75cc68"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_ringType</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#dee4f3431027813095272c568fc6b5ce"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#dee4f3431027813095272c568fc6b5ce"><span class="id" title="notation">ringType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#dee4f3431027813095272c568fc6b5ce"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#dee4f3431027813095272c568fc6b5ce"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="primeChar_scale"><span class="id" title="definition">primeChar_scale</span></a> <span class="id" title="var">a</span> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.field.finfield.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Let</span> <a name="PrimeChar.PrimeCharRing.natrFp"><span class="id" title="variable">natrFp</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><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.field.finfield.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">F_p</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">)%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.finfield.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="primeChar_scaleA"><span class="id" title="lemma">primeChar_scaleA</span></a> <span class="id" title="var">a</span> <span class="id" title="var">b</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.field.finfield.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.field.finfield.html#5f6f59b8095d2eaa0b5a55ed9129580f"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.field.finfield.html#5f6f59b8095d2eaa0b5a55ed9129580f"><span class="id" title="notation">p</span></a><a class="idref" href="mathcomp.field.finfield.html#5f6f59b8095d2eaa0b5a55ed9129580f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.finfield.html#5f6f59b8095d2eaa0b5a55ed9129580f"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.finfield.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="mathcomp.field.finfield.html#5f6f59b8095d2eaa0b5a55ed9129580f"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.field.finfield.html#5f6f59b8095d2eaa0b5a55ed9129580f"><span class="id" title="notation">p</span></a><a class="idref" href="mathcomp.field.finfield.html#5f6f59b8095d2eaa0b5a55ed9129580f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.field.finfield.html#5f6f59b8095d2eaa0b5a55ed9129580f"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.finfield.html#5f6f59b8095d2eaa0b5a55ed9129580f"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.finfield.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.finfield.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="mathcomp.field.finfield.html#5f6f59b8095d2eaa0b5a55ed9129580f"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.field.finfield.html#5f6f59b8095d2eaa0b5a55ed9129580f"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.field.finfield.html#5f6f59b8095d2eaa0b5a55ed9129580f"><span class="id" title="notation">p</span></a><a class="idref" href="mathcomp.field.finfield.html#5f6f59b8095d2eaa0b5a55ed9129580f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="primeChar_scale1"><span class="id" title="lemma">primeChar_scale1</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#left_id"><span class="id" title="definition">left_id</span></a> 1 <a class="idref" href="mathcomp.field.finfield.html#primeChar_scale"><span class="id" title="definition">primeChar_scale</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="primeChar_scaleDr"><span class="id" title="lemma">primeChar_scaleDr</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#right_distributive"><span class="id" title="definition">right_distributive</span></a> <a class="idref" href="mathcomp.field.finfield.html#primeChar_scale"><span class="id" title="definition">primeChar_scale</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#327bb2f0da6fd7c01a004dedcfc2dee4"><span class="id" title="notation">+%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#327bb2f0da6fd7c01a004dedcfc2dee4"><span class="id" title="notation">R</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="primeChar_scaleDl"><span class="id" title="lemma">primeChar_scaleDl</span></a> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.field.finfield.html#primeChar_scale"><span class="id" title="definition">primeChar_scale</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#8f28bbd804547edd8de802d63ef85617"><span class="id" title="notation">^~</span></a> <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">:</span></a> <span class="id" title="var">a</span> <span class="id" title="var">b</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.field.finfield.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.finfield.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">}</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="primeChar_lmodMixin"><span class="id" title="definition">primeChar_lmodMixin</span></a> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Lmodule.Exports.LmodMixin"><span class="id" title="abbreviation">LmodMixin</span></a> <a class="idref" href="mathcomp.field.finfield.html#primeChar_scaleA"><span class="id" title="lemma">primeChar_scaleA</span></a> <a class="idref" href="mathcomp.field.finfield.html#primeChar_scale1"><span class="id" title="lemma">primeChar_scale1</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.field.finfield.html#primeChar_scaleDr"><span class="id" title="lemma">primeChar_scaleDr</span></a> <a class="idref" href="mathcomp.field.finfield.html#primeChar_scaleDl"><span class="id" title="lemma">primeChar_scaleDl</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_lmodType</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Lmodule.Exports.LmodType"><span class="id" title="abbreviation">LmodType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#primeChar_lmodMixin"><span class="id" title="definition">primeChar_lmodMixin</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="primeChar_scaleAl"><span class="id" title="lemma">primeChar_scaleAl</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Lalgebra.axiom"><span class="id" title="definition">GRing.Lalgebra.axiom</span></a> ( <a class="idref" href="mathcomp.algebra.ssralg.html#d5d4e2467843f67554f1a8a22d125de9"><span class="id" title="notation">*%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d5d4e2467843f67554f1a8a22d125de9"><span class="id" title="notation">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a>).<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_LalgType</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Lalgebra.Exports.LalgType"><span class="id" title="abbreviation">LalgType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#primeChar_scaleAl"><span class="id" title="lemma">primeChar_scaleAl</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="primeChar_scaleAr"><span class="id" title="lemma">primeChar_scaleAr</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Algebra.axiom"><span class="id" title="definition">GRing.Algebra.axiom</span></a> <a class="idref" href="mathcomp.field.finfield.html#primeChar_LalgType"><span class="id" title="definition">primeChar_LalgType</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_algType</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Algebra.Exports.AlgType"><span class="id" title="abbreviation">AlgType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#primeChar_scaleAr"><span class="id" title="lemma">primeChar_scaleAr</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.PrimeCharRing"><span class="id" title="section">PrimeCharRing</span></a>.<br/>
+
+<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_unitRingType</span> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.UnitRing.Exports.unitRingType"><span class="id" title="abbreviation">unitRingType</span></a>) <span class="id" title="var">charRp</span> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.ssralg.html#f02859ca87d7563e473a6ba817bdc33f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#f02859ca87d7563e473a6ba817bdc33f"><span class="id" title="notation">unitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#f02859ca87d7563e473a6ba817bdc33f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#charRp"><span class="id" title="variable">charRp</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#f02859ca87d7563e473a6ba817bdc33f"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_unitAlgType</span> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.UnitRing.Exports.unitRingType"><span class="id" title="abbreviation">unitRingType</span></a>) <span class="id" title="var">charRp</span> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.ssralg.html#bdb1eed686184a9a4099efa772be7bc7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#bdb1eed686184a9a4099efa772be7bc7"><span class="id" title="notation">unitAlgType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#bdb1eed686184a9a4099efa772be7bc7"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#charRp"><span class="id" title="variable">charRp</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#bdb1eed686184a9a4099efa772be7bc7"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_comRingType</span> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ComRing.Exports.comRingType"><span class="id" title="abbreviation">comRingType</span></a>) <span class="id" title="var">charRp</span> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.ssralg.html#57b384122345a94c564987d4b6ee9f0f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#57b384122345a94c564987d4b6ee9f0f"><span class="id" title="notation">comRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#57b384122345a94c564987d4b6ee9f0f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#charRp"><span class="id" title="variable">charRp</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#57b384122345a94c564987d4b6ee9f0f"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_comUnitRingType</span> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ComUnitRing.Exports.comUnitRingType"><span class="id" title="abbreviation">comUnitRingType</span></a>) <span class="id" title="var">charRp</span> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">comUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#charRp"><span class="id" title="variable">charRp</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_idomainType</span> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.Exports.idomainType"><span class="id" title="abbreviation">idomainType</span></a>) <span class="id" title="var">charRp</span> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.ssralg.html#9894f8fff6e44a40eb9fd9cfcbde7780"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9894f8fff6e44a40eb9fd9cfcbde7780"><span class="id" title="notation">idomainType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#9894f8fff6e44a40eb9fd9cfcbde7780"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#charRp"><span class="id" title="variable">charRp</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9894f8fff6e44a40eb9fd9cfcbde7780"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_fieldType</span> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.fieldType"><span class="id" title="abbreviation">fieldType</span></a>) <span class="id" title="var">charFp</span> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.ssralg.html#005edfce3bb0bbe988e3333ca30adc0f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#005edfce3bb0bbe988e3333ca30adc0f"><span class="id" title="notation">fieldType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#005edfce3bb0bbe988e3333ca30adc0f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="mathcomp.field.finfield.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.field.finfield.html#charFp"><span class="id" title="variable">charFp</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#005edfce3bb0bbe988e3333ca30adc0f"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="PrimeChar.FinRing"><span class="id" title="section">FinRing</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="PrimeChar.FinRing.R0"><span class="id" title="variable">R0</span></a> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Ring.Exports.finRingType"><span class="id" title="abbreviation">finRingType</span></a>) (<a name="PrimeChar.FinRing.charRp"><span class="id" title="variable">charRp</span></a> : <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.finfield.html#R0"><span class="id" title="variable">R0</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">]</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_finType</span> := <a class="idref" href="mathcomp.ssreflect.fintype.html#eb1f7a25d8e03f1f02a5769831d0e74e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#eb1f7a25d8e03f1f02a5769831d0e74e"><span class="id" title="notation">finType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#eb1f7a25d8e03f1f02a5769831d0e74e"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#eb1f7a25d8e03f1f02a5769831d0e74e"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_finZmodType</span> := <a class="idref" href="mathcomp.algebra.finalg.html#2980bb304205aec85bc1eeb5d0a573a5"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#2980bb304205aec85bc1eeb5d0a573a5"><span class="id" title="notation">finZmodType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#2980bb304205aec85bc1eeb5d0a573a5"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.algebra.finalg.html#2980bb304205aec85bc1eeb5d0a573a5"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_baseGroupType</span> := <a class="idref" href="mathcomp.algebra.finalg.html#ee332ddd6e3626489ee70ea4c624f1cd"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#ee332ddd6e3626489ee70ea4c624f1cd"><span class="id" title="notation">baseFinGroupType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#ee332ddd6e3626489ee70ea4c624f1cd"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#ee332ddd6e3626489ee70ea4c624f1cd"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#ee332ddd6e3626489ee70ea4c624f1cd"><span class="id" title="notation">+%</span></a><a class="idref" href="mathcomp.algebra.finalg.html#ee332ddd6e3626489ee70ea4c624f1cd"><span class="id" title="notation">R</span></a><a class="idref" href="mathcomp.algebra.finalg.html#ee332ddd6e3626489ee70ea4c624f1cd"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_groupType</span> := <a class="idref" href="mathcomp.algebra.finalg.html#ad4d9ed93eeed8e8e57c81c6e35699c4"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#ad4d9ed93eeed8e8e57c81c6e35699c4"><span class="id" title="notation">finGroupType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#ad4d9ed93eeed8e8e57c81c6e35699c4"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#ad4d9ed93eeed8e8e57c81c6e35699c4"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#ad4d9ed93eeed8e8e57c81c6e35699c4"><span class="id" title="notation">+%</span></a><a class="idref" href="mathcomp.algebra.finalg.html#ad4d9ed93eeed8e8e57c81c6e35699c4"><span class="id" title="notation">R</span></a><a class="idref" href="mathcomp.algebra.finalg.html#ad4d9ed93eeed8e8e57c81c6e35699c4"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_finRingType</span> := <a class="idref" href="mathcomp.algebra.finalg.html#cf58bd711195f609ec57107fc402496c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#cf58bd711195f609ec57107fc402496c"><span class="id" title="notation">finRingType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#cf58bd711195f609ec57107fc402496c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.algebra.finalg.html#cf58bd711195f609ec57107fc402496c"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_finLmodType</span> := <a class="idref" href="mathcomp.algebra.finalg.html#73928e07fdf596d7d0d44cccaf9a9cb3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#73928e07fdf596d7d0d44cccaf9a9cb3"><span class="id" title="notation">finLmodType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#73928e07fdf596d7d0d44cccaf9a9cb3"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.algebra.finalg.html#73928e07fdf596d7d0d44cccaf9a9cb3"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_finLalgType</span> := <a class="idref" href="mathcomp.algebra.finalg.html#f791552e58608a16cb248da4e7f34691"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#f791552e58608a16cb248da4e7f34691"><span class="id" title="notation">finLalgType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#f791552e58608a16cb248da4e7f34691"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.algebra.finalg.html#f791552e58608a16cb248da4e7f34691"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_finAlgType</span> := <a class="idref" href="mathcomp.algebra.finalg.html#1f3938acab41e5853e751c34c441bf83"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#1f3938acab41e5853e751c34c441bf83"><span class="id" title="notation">finAlgType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#1f3938acab41e5853e751c34c441bf83"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.algebra.finalg.html#1f3938acab41e5853e751c34c441bf83"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Let</span> <a name="PrimeChar.FinRing.pr_p"><span class="id" title="variable">pr_p</span></a> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.p"><span class="id" title="variable">p</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="primeChar_abelem"><span class="id" title="lemma">primeChar_abelem</span></a> : <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.abelian.html#bcb4124a3d9b102768b81d5d3006e029"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.abelian.html#bcb4124a3d9b102768b81d5d3006e029"><span class="id" title="notation">abelem</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="primeChar_pgroup"><span class="id" title="lemma">primeChar_pgroup</span></a> : <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="order_primeChar"><span class="id" title="lemma">order_primeChar</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#9e45f909d1732d6d9e153b650829bccf"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="mathcomp.ssreflect.eqtype.html#9e45f909d1732d6d9e153b650829bccf"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#89402f0d9375903caa99ad84144160d5"><span class="id" title="notation">#[</span></a><a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#89402f0d9375903caa99ad84144160d5"><span class="id" title="notation">]</span></a>%<span class="id" title="var">g</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.p"><span class="id" title="variable">p</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Let</span> <a name="PrimeChar.FinRing.n"><span class="id" title="variable">n</span></a> := <a class="idref" href="mathcomp.ssreflect.prime.html#logn"><span class="id" title="definition">logn</span></a> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_primeChar"><span class="id" title="lemma">card_primeChar</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.field.finfield.html#PrimeChar.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.FinRing.n"><span class="id" title="variable">n</span></a>)%<span class="id" title="var">N</span>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="primeChar_vectAxiom"><span class="id" title="lemma">primeChar_vectAxiom</span></a> : <a class="idref" href="mathcomp.algebra.vector.html#Vector.axiom"><span class="id" title="abbreviation">Vector.axiom</span></a> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.FinRing.n"><span class="id" title="variable">n</span></a> (<a class="idref" href="mathcomp.field.finfield.html#primeChar_lmodType"><span class="id" title="definition">primeChar_lmodType</span></a> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.FinRing.charRp"><span class="id" title="variable">charRp</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="primeChar_vectMixin"><span class="id" title="definition">primeChar_vectMixin</span></a> := <a class="idref" href="mathcomp.algebra.vector.html#Vector.Mixin"><span class="id" title="constructor">Vector.Mixin</span></a> <a class="idref" href="mathcomp.field.finfield.html#primeChar_vectAxiom"><span class="id" title="lemma">primeChar_vectAxiom</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_vectType</span> := <a class="idref" href="mathcomp.algebra.vector.html#Vector.Exports.VectType"><span class="id" title="abbreviation">VectType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#primeChar_vectMixin"><span class="id" title="definition">primeChar_vectMixin</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="primeChar_dimf"><span class="id" title="lemma">primeChar_dimf</span></a> : <a class="idref" href="mathcomp.algebra.vector.html#ee35a6780ccd60155a3be89dcb5fdb30"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.vector.html#ee35a6780ccd60155a3be89dcb5fdb30"><span class="id" title="notation">dim</span></a> <a class="idref" href="mathcomp.algebra.vector.html#899a5fd19c4f3564d9757a9ac446b1dc"><span class="id" title="notation">{:</span></a><a class="idref" href="mathcomp.field.finfield.html#primeChar_vectType"><span class="id" title="definition">primeChar_vectType</span></a><a class="idref" href="mathcomp.algebra.vector.html#899a5fd19c4f3564d9757a9ac446b1dc"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.FinRing.n"><span class="id" title="variable">n</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.FinRing"><span class="id" title="section">FinRing</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_finUnitRingType</span> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.UnitRing.Exports.finUnitRingType"><span class="id" title="abbreviation">finUnitRingType</span></a>) <span class="id" title="var">charRp</span> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.finalg.html#7f21453830587186138043335ab91dd1"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#7f21453830587186138043335ab91dd1"><span class="id" title="notation">finUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#7f21453830587186138043335ab91dd1"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#charRp"><span class="id" title="variable">charRp</span></a><a class="idref" href="mathcomp.algebra.finalg.html#7f21453830587186138043335ab91dd1"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_finUnitAlgType</span> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.UnitRing.Exports.finUnitRingType"><span class="id" title="abbreviation">finUnitRingType</span></a>) <span class="id" title="var">charRp</span> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.finalg.html#9af0def31728327fea663946c68b8952"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#9af0def31728327fea663946c68b8952"><span class="id" title="notation">finUnitAlgType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#9af0def31728327fea663946c68b8952"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#charRp"><span class="id" title="variable">charRp</span></a><a class="idref" href="mathcomp.algebra.finalg.html#9af0def31728327fea663946c68b8952"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_FalgType</span> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.UnitRing.Exports.finUnitRingType"><span class="id" title="abbreviation">finUnitRingType</span></a>) <span class="id" title="var">charRp</span> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.field.falgebra.html#3c0387428f19a365dfa0c989db9030d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.field.falgebra.html#3c0387428f19a365dfa0c989db9030d7"><span class="id" title="notation">FalgType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.field.falgebra.html#3c0387428f19a365dfa0c989db9030d7"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#charRp"><span class="id" title="variable">charRp</span></a><a class="idref" href="mathcomp.field.falgebra.html#3c0387428f19a365dfa0c989db9030d7"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_finComRingType</span> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.ComRing.Exports.finComRingType"><span class="id" title="abbreviation">finComRingType</span></a>) <span class="id" title="var">charRp</span> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.finalg.html#381777e14bce98b548cb274563c7fc56"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#381777e14bce98b548cb274563c7fc56"><span class="id" title="notation">finComRingType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#381777e14bce98b548cb274563c7fc56"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#charRp"><span class="id" title="variable">charRp</span></a><a class="idref" href="mathcomp.algebra.finalg.html#381777e14bce98b548cb274563c7fc56"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_finComUnitRingType</span> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.ComUnitRing.Exports.finComUnitRingType"><span class="id" title="abbreviation">finComUnitRingType</span></a>) <span class="id" title="var">charRp</span> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.finalg.html#f0aa4fcf143660f4378ecfead8f3fdda"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#f0aa4fcf143660f4378ecfead8f3fdda"><span class="id" title="notation">finComUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#f0aa4fcf143660f4378ecfead8f3fdda"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#charRp"><span class="id" title="variable">charRp</span></a><a class="idref" href="mathcomp.algebra.finalg.html#f0aa4fcf143660f4378ecfead8f3fdda"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_finIdomainType</span> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.IntegralDomain.Exports.finIdomainType"><span class="id" title="abbreviation">finIdomainType</span></a>) <span class="id" title="var">charRp</span> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.finalg.html#6c49b73b4d6aa1a932fafe7684bba39c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#6c49b73b4d6aa1a932fafe7684bba39c"><span class="id" title="notation">finIdomainType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#6c49b73b4d6aa1a932fafe7684bba39c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#charRp"><span class="id" title="variable">charRp</span></a><a class="idref" href="mathcomp.algebra.finalg.html#6c49b73b4d6aa1a932fafe7684bba39c"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="PrimeChar.FinField"><span class="id" title="section">FinField</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="PrimeChar.FinField.F0"><span class="id" title="variable">F0</span></a> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Field.Exports.finFieldType"><span class="id" title="abbreviation">finFieldType</span></a>) (<a name="PrimeChar.FinField.charFp"><span class="id" title="variable">charFp</span></a> : <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.finfield.html#F0"><span class="id" title="variable">F0</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">]</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_finFieldType</span> := <a class="idref" href="mathcomp.algebra.finalg.html#07fdfbae2c02044f4dae6b5dbeb0c7c7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#07fdfbae2c02044f4dae6b5dbeb0c7c7"><span class="id" title="notation">finFieldType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#07fdfbae2c02044f4dae6b5dbeb0c7c7"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#F"><span class="id" title="abbreviation">F</span></a><a class="idref" href="mathcomp.algebra.finalg.html#07fdfbae2c02044f4dae6b5dbeb0c7c7"><span class="id" title="notation">]</span></a>.<br/>
+</div>
+
+<div class="doc">
+ We need to use the eta-long version of the constructor here as projections 
+ of the Canonical fieldType of F cannot be computed syntactically.           
+</div>
+<div class="code">
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_fieldExtType</span> := <a class="idref" href="mathcomp.field.fieldext.html#5f5a3c95feae5e889ef0ed2ea21bd611"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.field.fieldext.html#5f5a3c95feae5e889ef0ed2ea21bd611"><span class="id" title="notation">fieldExtType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.field.fieldext.html#5f5a3c95feae5e889ef0ed2ea21bd611"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#F"><span class="id" title="abbreviation">F</span></a> <a class="idref" href="mathcomp.field.fieldext.html#5f5a3c95feae5e889ef0ed2ea21bd611"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.FinField.F0"><span class="id" title="variable">F0</span></a><a class="idref" href="mathcomp.field.fieldext.html#5f5a3c95feae5e889ef0ed2ea21bd611"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_splittingFieldType</span> := <a class="idref" href="mathcomp.field.finfield.html#FinSplittingFieldType"><span class="id" title="abbreviation">FinSplittingFieldType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.field.finfield.html#F"><span class="id" title="abbreviation">F</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.FinField"><span class="id" title="section">FinField</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar"><span class="id" title="section">PrimeChar</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="FinSplittingField"><span class="id" title="section">FinSplittingField</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="FinSplittingField.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Field.Exports.finFieldType"><span class="id" title="abbreviation">finFieldType</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ By card_vspace order K = #|K| for any finType structure on L; however we   
+ do not want to impose the FinVector instance here.                          
+</div>
+<div class="code">
+<span class="id" title="keyword">Let</span> <a name="FinSplittingField.order"><span class="id" title="variable">order</span></a> (<span class="id" title="var">L</span> : <a class="idref" href="mathcomp.algebra.vector.html#Vector.Exports.vectType"><span class="id" title="abbreviation">vectType</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinSplittingField.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">K</span> : <a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">vspace</span></a> <a class="idref" href="mathcomp.field.finfield.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">}</span></a>) := (<a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.field.finfield.html#FinSplittingField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.vector.html#ee35a6780ccd60155a3be89dcb5fdb30"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.vector.html#ee35a6780ccd60155a3be89dcb5fdb30"><span class="id" title="notation">dim</span></a> <a class="idref" href="mathcomp.field.finfield.html#K"><span class="id" title="variable">K</span></a>)%<span class="id" title="var">N</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="FinSplittingField.FinGalois"><span class="id" title="section">FinGalois</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="FinSplittingField.FinGalois.L"><span class="id" title="variable">L</span></a> : <a class="idref" href="mathcomp.field.galois.html#SplittingField.Exports.splittingFieldType"><span class="id" title="abbreviation">splittingFieldType</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinSplittingField.F"><span class="id" title="variable">F</span></a>.<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">a</span> <span class="id" title="var">b</span> : <a class="idref" href="mathcomp.field.finfield.html#FinSplittingField.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.field.finfield.html#FinSplittingField.FinGalois.L"><span class="id" title="variable">L</span></a>) (<span class="id" title="var">K</span> <span class="id" title="var">E</span> : <a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">subfield</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinSplittingField.FinGalois.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">}</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Let</span> <a name="FinSplittingField.FinGalois.galL"><span class="id" title="variable">galL</span></a> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.field.galois.html#galois"><span class="id" title="definition">galois</span></a> <a class="idref" href="mathcomp.field.finfield.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.algebra.vector.html#899a5fd19c4f3564d9757a9ac446b1dc"><span class="id" title="notation">{:</span></a><a class="idref" href="mathcomp.field.finfield.html#FinSplittingField.FinGalois.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.vector.html#899a5fd19c4f3564d9757a9ac446b1dc"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Fact</span> <a name="galLgen"><span class="id" title="lemma">galLgen</span></a> <span class="id" title="var">K</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">{</span></a><span class="id" title="var">alpha</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.cyclic.html#generator"><span class="id" title="definition">generator</span></a> <a class="idref" href="mathcomp.field.galois.html#7f39fd713ca3f00fbfda8b71eae7e2e1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.galois.html#7f39fd713ca3f00fbfda8b71eae7e2e1"><span class="id" title="notation">Gal</span></a><a class="idref" href="mathcomp.field.galois.html#7f39fd713ca3f00fbfda8b71eae7e2e1"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.vector.html#899a5fd19c4f3564d9757a9ac446b1dc"><span class="id" title="notation">{:</span></a><a class="idref" href="mathcomp.field.finfield.html#FinSplittingField.FinGalois.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.vector.html#899a5fd19c4f3564d9757a9ac446b1dc"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.field.galois.html#7f39fd713ca3f00fbfda8b71eae7e2e1"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.field.finfield.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.galois.html#7f39fd713ca3f00fbfda8b71eae7e2e1"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.field.finfield.html#alpha"><span class="id" title="variable">alpha</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">&amp;</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.field.finfield.html#alpha"><span class="id" title="variable">alpha</span></a> <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinSplittingField.order"><span class="id" title="variable">order</span></a> <a class="idref" href="mathcomp.field.finfield.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="finField_galois"><span class="id" title="lemma">finField_galois</span></a> <span class="id" title="var">K</span> <span class="id" title="var">E</span> : (<a class="idref" href="mathcomp.field.finfield.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.algebra.vector.html#755d11a7d5629bce3486e7cbadc915e7"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.finfield.html#E"><span class="id" title="variable">E</span></a>)%<span class="id" title="var">VS</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.galois.html#galois"><span class="id" title="definition">galois</span></a> <a class="idref" href="mathcomp.field.finfield.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.finfield.html#E"><span class="id" title="variable">E</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="finField_galois_generator"><span class="id" title="lemma">finField_galois_generator</span></a> <span class="id" title="var">K</span> <span class="id" title="var">E</span> :<br/>
+&nbsp;&nbsp;&nbsp;(<a class="idref" href="mathcomp.field.finfield.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.algebra.vector.html#755d11a7d5629bce3486e7cbadc915e7"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.finfield.html#E"><span class="id" title="variable">E</span></a>)%<span class="id" title="var">VS</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
+&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">{</span></a><span class="id" title="var">alpha</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.cyclic.html#generator"><span class="id" title="definition">generator</span></a> <a class="idref" href="mathcomp.field.galois.html#7f39fd713ca3f00fbfda8b71eae7e2e1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.galois.html#7f39fd713ca3f00fbfda8b71eae7e2e1"><span class="id" title="notation">Gal</span></a><a class="idref" href="mathcomp.field.galois.html#7f39fd713ca3f00fbfda8b71eae7e2e1"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.finfield.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="mathcomp.field.galois.html#7f39fd713ca3f00fbfda8b71eae7e2e1"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.field.finfield.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.galois.html#7f39fd713ca3f00fbfda8b71eae7e2e1"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.field.finfield.html#alpha"><span class="id" title="variable">alpha</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.finfield.html#E"><span class="id" title="variable">E</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.field.finfield.html#alpha"><span class="id" title="variable">alpha</span></a> <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinSplittingField.order"><span class="id" title="variable">order</span></a> <a class="idref" href="mathcomp.field.finfield.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#FinSplittingField.FinGalois"><span class="id" title="section">FinGalois</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="Fermat's_little_theorem"><span class="id" title="lemma">Fermat's_little_theorem</span></a> (<span class="id" title="var">L</span> : <a class="idref" href="mathcomp.field.fieldext.html#FieldExt.Exports.fieldExtType"><span class="id" title="abbreviation">fieldExtType</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinSplittingField.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">K</span> : <a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">subfield</span></a> <a class="idref" href="mathcomp.field.finfield.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">}</span></a>) <span class="id" title="var">a</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.finfield.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.finfield.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.finfield.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinSplittingField.order"><span class="id" title="variable">order</span></a> <a class="idref" href="mathcomp.field.finfield.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.finfield.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#FinSplittingField"><span class="id" title="section">FinSplittingField</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="FinFieldExists"><span class="id" title="section">FinFieldExists</span></a>.<br/>
+</div>
+
+<div class="doc">
+ While he existence of finite splitting fields and of finite fields of      
+ arbitrary prime power order is mathematically straightforward, it is       
+ technically challenging to formalize in Coq. The Coq typechecker performs  
+ poorly for the spme of the deeply nested dependent types used in the       
+ construction, such as polynomials over extensions of extensions of finite  
+ fields. Any conversion in a nested structure parameter incurs a huge       
+ overhead as it is shared across term comparison by call-by-need evalution. 
+ The proof of FinSplittingFieldFor is contrived to mitigate this effect:    
+ the abbreviation map_poly_extField alone divides by 3 the proof checking   
+ time, by reducing the number of occurrences of field(Ext)Type structures   
+ in the subgoals; the succesive, apparently redundant 'suffices' localize   
+ some of the conversions to smaller subgoals, yielding a further 8-fold     
+ time gain. In particular, we construct the splitting field as a subtype    
+ of a recursive construction rather than prove that the latter yields       
+ precisely a splitting field.                                                
+<div class="paragraph"> </div>
+
+  The apparently redundant type annotation reduces checking time by 30%.      
+</div>
+<div class="code">
+<span class="id" title="keyword">Let</span> <a name="FinFieldExists.map_poly_extField"><span class="id" title="variable">map_poly_extField</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.fieldType"><span class="id" title="abbreviation">fieldType</span></a>) (<span class="id" title="var">L</span> : <a class="idref" href="mathcomp.field.fieldext.html#FieldExt.Exports.fieldExtType"><span class="id" title="abbreviation">fieldExtType</span></a> <a class="idref" href="mathcomp.field.finfield.html#F"><span class="id" title="variable">F</span></a>) :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Theory.in_alg"><span class="id" title="abbreviation">in_alg</span></a> <a class="idref" href="mathcomp.field.finfield.html#L"><span class="id" title="variable">L</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.field.finfield.html#F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.field.finfield.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FinSplittingFieldFor"><span class="id" title="lemma">FinSplittingFieldFor</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Field.Exports.finFieldType"><span class="id" title="abbreviation">finFieldType</span></a>) (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.field.finfield.html#F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}</span></a>) :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.field.finfield.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">{</span></a><span class="id" title="var">L</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.galois.html#SplittingField.Exports.splittingFieldType"><span class="id" title="abbreviation">splittingFieldType</span></a> <a class="idref" href="mathcomp.field.finfield.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.field.galois.html#splittingFieldFor"><span class="id" title="definition">splittingFieldFor</span></a> 1 <a class="idref" href="mathcomp.field.finfield.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.field.finfield.html#445fdb3ebc0ff682c0cd1af9d3a32b17"><span class="id" title="notation">^%:</span></a><a class="idref" href="mathcomp.field.finfield.html#445fdb3ebc0ff682c0cd1af9d3a32b17"><span class="id" title="notation">A</span></a> <a class="idref" href="mathcomp.algebra.vector.html#899a5fd19c4f3564d9757a9ac446b1dc"><span class="id" title="notation">{:</span></a><a class="idref" href="mathcomp.field.finfield.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.vector.html#899a5fd19c4f3564d9757a9ac446b1dc"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="PrimePowerField"><span class="id" title="lemma">PrimePowerField</span></a> <span class="id" title="var">p</span> <span class="id" title="var">k</span> (<span class="id" title="var">m</span> := (<a class="idref" href="mathcomp.field.finfield.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.field.finfield.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">N</span>) :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.field.finfield.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> 0 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.field.finfield.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">{</span></a><span class="id" title="var">Fm</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Field.Exports.finFieldType"><span class="id" title="abbreviation">finFieldType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.field.finfield.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.finfield.html#Fm"><span class="id" title="variable">Fm</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.field.finfield.html#Fm"><span class="id" title="variable">Fm</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.finfield.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#FinFieldExists"><span class="id" title="section">FinFieldExists</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="FinDomain"><span class="id" title="section">FinDomain</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Import</span> <span class="id" title="var">ssrnum</span> <span class="id" title="var">ssrint</span> <span class="id" title="var">algC</span> <span class="id" title="var">cyclotomic</span> <span class="id" title="var">Num.Theory</span>.<br/>
+<span class="comment">(*&nbsp;Hide&nbsp;polynomial&nbsp;divisibility.&nbsp;*)</span><br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="FinDomain.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.UnitRing.Exports.finUnitRingType"><span class="id" title="abbreviation">finUnitRingType</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Hypothesis</span> <a name="FinDomain.domR"><span class="id" title="variable">domR</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.axiom"><span class="id" title="definition">GRing.IntegralDomain.axiom</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a>.<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> : <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Let</span> <a name="FinDomain.lregR"><span class="id" title="variable">lregR</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.lreg"><span class="id" title="definition">GRing.lreg</span></a> <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="finDomain_field"><span class="id" title="lemma">finDomain_field</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="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ This is Witt's proof of Wedderburn's little theorem.  
+</div>
+<div class="code">
+<span class="id" title="keyword">Theorem</span> <a name="finDomain_mulrC"><span class="id" title="lemma">finDomain_mulrC</span></a> : @<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#commutative"><span class="id" title="definition">commutative</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d5d4e2467843f67554f1a8a22d125de9"><span class="id" title="notation">*%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d5d4e2467843f67554f1a8a22d125de9"><span class="id" title="notation">R</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="FinDomainFieldType"><span class="id" title="definition">FinDomainFieldType</span></a> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Field.Exports.finFieldType"><span class="id" title="abbreviation">finFieldType</span></a> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">fin_unit_class</span> := <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.UnitRing.class"><span class="id" title="definition">FinRing.UnitRing.class</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a> <span class="id" title="tactic">in</span><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">com_class</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ComRing.Class"><span class="id" title="constructor">GRing.ComRing.Class</span></a> <a class="idref" href="mathcomp.field.finfield.html#finDomain_mulrC"><span class="id" title="lemma">finDomain_mulrC</span></a> <span class="id" title="tactic">in</span><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">com_unit_class</span> := @<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ComUnitRing.Class"><span class="id" title="constructor">GRing.ComUnitRing.Class</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#com_class"><span class="id" title="variable">com_class</span></a> <a class="idref" href="mathcomp.field.finfield.html#fin_unit_class"><span class="id" title="variable">fin_unit_class</span></a> <span class="id" title="tactic">in</span><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">dom_class</span> := @<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.Class"><span class="id" title="constructor">GRing.IntegralDomain.Class</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#com_unit_class"><span class="id" title="variable">com_unit_class</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomain.domR"><span class="id" title="variable">domR</span></a> <span class="id" title="tactic">in</span><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">field_class</span> := @<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Class"><span class="id" title="constructor">GRing.Field.Class</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#dom_class"><span class="id" title="variable">dom_class</span></a> <a class="idref" href="mathcomp.field.finfield.html#finDomain_field"><span class="id" title="lemma">finDomain_field</span></a> <span class="id" title="tactic">in</span><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">finfield_class</span> := @<a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Field.Class"><span class="id" title="constructor">FinRing.Field.Class</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#field_class"><span class="id" title="variable">field_class</span></a> <a class="idref" href="mathcomp.field.finfield.html#fin_unit_class"><span class="id" title="variable">fin_unit_class</span></a> <span class="id" title="tactic">in</span><br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Field.Pack"><span class="id" title="constructor">FinRing.Field.Pack</span></a> <a class="idref" href="mathcomp.field.finfield.html#finfield_class"><span class="id" title="variable">finfield_class</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="FinDomainSplittingFieldType"><span class="id" title="definition">FinDomainSplittingFieldType</span></a> <span class="id" title="var">p</span> (<span class="id" title="var">charRp</span> : <a class="idref" href="mathcomp.field.finfield.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">]</span></a>) :=<br/>
+&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">RoverFp</span> := @<a class="idref" href="mathcomp.field.finfield.html#primeChar_splittingFieldType"><span class="id" title="definition">primeChar_splittingFieldType</span></a> <a class="idref" href="mathcomp.field.finfield.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomainFieldType"><span class="id" title="definition">FinDomainFieldType</span></a> <a class="idref" href="mathcomp.field.finfield.html#charRp"><span class="id" title="variable">charRp</span></a> <span class="id" title="tactic">in</span><br/>
+&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.field.galois.html#201f8b6ebe31f6a88a3d073a45335fc2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.field.galois.html#201f8b6ebe31f6a88a3d073a45335fc2"><span class="id" title="notation">splittingFieldType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#ac70144de8117a1d767eef28420399d1"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.field.galois.html#201f8b6ebe31f6a88a3d073a45335fc2"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.galois.html#201f8b6ebe31f6a88a3d073a45335fc2"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.field.finfield.html#RoverFp"><span class="id" title="variable">RoverFp</span></a><a class="idref" href="mathcomp.field.galois.html#201f8b6ebe31f6a88a3d073a45335fc2"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#FinDomain"><span class="id" title="section">FinDomain</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
author	Enrico Tassi	2018-04-20 10:54:22 +0200
committer	Enrico Tassi	2018-04-20 10:54:22 +0200
commit	ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch)
tree	e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.field.finfield.html
parent	3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)