htmldoc regenerated

author: Enrico Tassi 2019-05-22 13:43:08 +0200
committer: Enrico Tassi 2019-05-22 15:34:14 +0200
commit: 748d716efb2f2f75946c8386e441ce1789806a39 (patch)
tree: fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/mathcomp.field.finfield.html
parent: 415be3b908daadabf178a292c885db78e5b2c9a4 (diff)
1 files changed, 88 insertions, 89 deletions
diff --git a/docs/htmldoc/mathcomp.field.finfield.html b/docs/htmldoc/mathcomp.field.finfield.html
index c6454db..398b5de 100644
--- a/docs/htmldoc/mathcomp.field.finfield.html
+++ b/docs/htmldoc/mathcomp.field.finfield.html
@@ -21,7 +21,6 @@
 <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>
@@ -90,10 +89,10 @@
 <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/>
+<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#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinRing.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><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/>
+<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#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><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/>
@@ -105,26 +104,26 @@
 <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/>
+<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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#18d0918a160c839bc9f32d8e64dd406d"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.finalg.html#18d0918a160c839bc9f32d8e64dd406d"><span class="id" title="notation">unit</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.finalg.html#18d0918a160c839bc9f32d8e64dd406d"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f953bf7095e0da1cb644443fd0e17d6d"><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/>
+<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#c385a484ee9d1b4e0615924561a9b75e"><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/V8.9.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/>
+<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#663140372ac3b275aae871b74b140513"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><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/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><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/>
+<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#e809881bcf0cc80f806c17b9ef433187"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#e809881bcf0cc80f806c17b9ef433187"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#e809881bcf0cc80f806c17b9ef433187"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#51dc792c356ca1a71a3094b50d6bb2fb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">X</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#bba809eef925bb2b4e421c8b99ce8372"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#bba809eef925bb2b4e421c8b99ce8372"><span class="id" title="notation">prod_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#bba809eef925bb2b4e421c8b99ce8372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">X</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#51dc792c356ca1a71a3094b50d6bb2fb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#bba809eef925bb2b4e421c8b99ce8372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><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/>
+<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/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">{</span></a><span class="id" title="var">p</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><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/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><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/>
+<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#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">]</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="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/>
+<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#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.field.finfield.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">]</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#FinField"><span class="id" title="section">FinField</span></a>.<br/>
@@ -140,23 +139,23 @@
 
 <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/>
+<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/V8.9.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>.<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/>
+<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#95065d7eff417cb87497b35ad25bda41"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.vector.html#95065d7eff417cb87497b35ad25bda41"><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#95065d7eff417cb87497b35ad25bda41"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.field.finfield.html#V"><span class="id" title="variable">V</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.vector.html#6d9094556d4642bd9374f6c3dcaee079"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.vector.html#6d9094556d4642bd9374f6c3dcaee079"><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/>
+<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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.algebra.vector.html#6a45c77a68f1019c1f3b35b71c415ac8"><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#6a45c77a68f1019c1f3b35b71c415ac8"><span class="id" title="notation">}</span></a>%<span class="id" title="var">VS</span><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><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/>
+<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/V8.9.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>.<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/>
+<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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|(</span></a>1%<span class="id" title="var">VS</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.vector.html#95065d7eff417cb87497b35ad25bda41"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.vector.html#95065d7eff417cb87497b35ad25bda41"><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#95065d7eff417cb87497b35ad25bda41"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">)|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><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/>
@@ -185,9 +184,9 @@
 <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/>
+<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#dfd62d789441026daed4d1ea30e2ff11"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11"><span class="id" title="notation">finRingType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fieldExt_finRingType</span> <span class="id" title="var">fT</span> := <a class="idref" href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11"><span class="id" title="notation">finRingType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#fT"><span class="id" title="variable">fT</span></a><a class="idref" href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fieldExt_finFieldType</span> <span class="id" title="var">fT</span> := <a class="idref" href="mathcomp.algebra.finalg.html#85a9f33cca8b2a31e30517c43d5ecb47"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#85a9f33cca8b2a31e30517c43d5ecb47"><span class="id" title="notation">finFieldType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#85a9f33cca8b2a31e30517c43d5ecb47"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#fT"><span class="id" title="variable">fT</span></a><a class="idref" href="mathcomp.algebra.finalg.html#85a9f33cca8b2a31e30517c43d5ecb47"><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/>
@@ -206,7 +205,7 @@
 <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/>
+<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/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">Section</span> <a name="PrimeChar.PrimeCharRing"><span class="id" title="section">PrimeCharRing</span></a>.<br/>
@@ -215,49 +214,49 @@
 <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/>
+<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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.PrimeCharRing.R0"><span class="id" title="variable">R0</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">]</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/>
+<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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.PrimeCharRing.R0"><span class="id" title="variable">R0</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><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#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a>) (<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/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_eqType</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><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#2b9222c46a529018a8ebb5be6355801c"><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#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><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#6cecb3ca492751e55998eec154506328"><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#97b11d2a158d9db11032c2626798c6ac"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#97b11d2a158d9db11032c2626798c6ac"><span class="id" title="notation">zmodType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#97b11d2a158d9db11032c2626798c6ac"><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#97b11d2a158d9db11032c2626798c6ac"><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#964cf6dee45a836ccf0bcd3d85de1071"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#964cf6dee45a836ccf0bcd3d85de1071"><span class="id" title="notation">ringType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#964cf6dee45a836ccf0bcd3d85de1071"><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#964cf6dee45a836ccf0bcd3d85de1071"><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/>
+<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#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><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/>
+<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#6411ed08724033ae48d2865f0380d533"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">)%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.finfield.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:&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/>
+<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#99d0e83cb5d8e3b8b8814aee93045e65"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.field.finfield.html#99d0e83cb5d8e3b8b8814aee93045e65"><span class="id" title="notation">p</span></a><a class="idref" href="mathcomp.field.finfield.html#99d0e83cb5d8e3b8b8814aee93045e65"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.finfield.html#99d0e83cb5d8e3b8b8814aee93045e65"><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#99d0e83cb5d8e3b8b8814aee93045e65"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.field.finfield.html#99d0e83cb5d8e3b8b8814aee93045e65"><span class="id" title="notation">p</span></a><a class="idref" href="mathcomp.field.finfield.html#99d0e83cb5d8e3b8b8814aee93045e65"><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#99d0e83cb5d8e3b8b8814aee93045e65"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.finfield.html#99d0e83cb5d8e3b8b8814aee93045e65"><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#2d0cfb150261028f4ebd2ba355623dcc"><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#99d0e83cb5d8e3b8b8814aee93045e65"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.field.finfield.html#99d0e83cb5d8e3b8b8814aee93045e65"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.field.finfield.html#99d0e83cb5d8e3b8b8814aee93045e65"><span class="id" title="notation">p</span></a><a class="idref" href="mathcomp.field.finfield.html#99d0e83cb5d8e3b8b8814aee93045e65"><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/>
+<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/V8.9.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/>
+<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/V8.9.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#a87d5ea2e207e69e5e474db24f56d4cb"><span class="id" title="notation">+%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#a87d5ea2e207e69e5e474db24f56d4cb"><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/>
+<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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#d89396f990d6b54d736cfe259e498cf4"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><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#c7f78cf1f6a5e4f664654f7d671ca752"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><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/>
+<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#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.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/>
+<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#3609d85e23333c9e68741ad96b416eec"><span class="id" title="notation">*%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#3609d85e23333c9e68741ad96b416eec"><span class="id" title="notation">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.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#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.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/>
+ <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#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.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/>
@@ -266,87 +265,87 @@
 
 <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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.ssralg.html#2734494507570795a22f59746d1c0f0e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2734494507570795a22f59746d1c0f0e"><span class="id" title="notation">unitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2734494507570795a22f59746d1c0f0e"><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#2734494507570795a22f59746d1c0f0e"><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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.ssralg.html#53130370ad22aac4f3ee8434dbc4850d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#53130370ad22aac4f3ee8434dbc4850d"><span class="id" title="notation">unitAlgType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#53130370ad22aac4f3ee8434dbc4850d"><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#53130370ad22aac4f3ee8434dbc4850d"><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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.ssralg.html#8b92acac231ba6173223cf75164fca3d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#8b92acac231ba6173223cf75164fca3d"><span class="id" title="notation">comRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#8b92acac231ba6173223cf75164fca3d"><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#8b92acac231ba6173223cf75164fca3d"><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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">comUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.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#2dfeb3fb2088b370ad93742d4f23a0dc"><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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.ssralg.html#b10128495340407de3c7b321ce0c78de"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b10128495340407de3c7b321ce0c78de"><span class="id" title="notation">idomainType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#b10128495340407de3c7b321ce0c78de"><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#b10128495340407de3c7b321ce0c78de"><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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.ssralg.html#be36f4c61e9a82f836d531a63f34e6c2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#be36f4c61e9a82f836d531a63f34e6c2"><span class="id" title="notation">fieldType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#be36f4c61e9a82f836d531a63f34e6c2"><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#be36f4c61e9a82f836d531a63f34e6c2"><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/>
+<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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.finfield.html#R0"><span class="id" title="variable">R0</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">]</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">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/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_finType</span> := <a class="idref" href="mathcomp.ssreflect.fintype.html#0e3773306b0834fa9a0572c7b198b77f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#0e3773306b0834fa9a0572c7b198b77f"><span class="id" title="notation">finType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#0e3773306b0834fa9a0572c7b198b77f"><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#0e3773306b0834fa9a0572c7b198b77f"><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#144f70011c058d1c741eaa431b4b8944"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#144f70011c058d1c741eaa431b4b8944"><span class="id" title="notation">finZmodType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#144f70011c058d1c741eaa431b4b8944"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.algebra.finalg.html#144f70011c058d1c741eaa431b4b8944"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_baseGroupType</span> := <a class="idref" href="mathcomp.algebra.finalg.html#d6b25f501b9fb5e9b743073d52f24511"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#d6b25f501b9fb5e9b743073d52f24511"><span class="id" title="notation">baseFinGroupType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#d6b25f501b9fb5e9b743073d52f24511"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#d6b25f501b9fb5e9b743073d52f24511"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#d6b25f501b9fb5e9b743073d52f24511"><span class="id" title="notation">+%</span></a><a class="idref" href="mathcomp.algebra.finalg.html#d6b25f501b9fb5e9b743073d52f24511"><span class="id" title="notation">R</span></a><a class="idref" href="mathcomp.algebra.finalg.html#d6b25f501b9fb5e9b743073d52f24511"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_groupType</span> := <a class="idref" href="mathcomp.algebra.finalg.html#a37f16a335f7a3ac65f83e3545c3e50c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#a37f16a335f7a3ac65f83e3545c3e50c"><span class="id" title="notation">finGroupType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#a37f16a335f7a3ac65f83e3545c3e50c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#a37f16a335f7a3ac65f83e3545c3e50c"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#a37f16a335f7a3ac65f83e3545c3e50c"><span class="id" title="notation">+%</span></a><a class="idref" href="mathcomp.algebra.finalg.html#a37f16a335f7a3ac65f83e3545c3e50c"><span class="id" title="notation">R</span></a><a class="idref" href="mathcomp.algebra.finalg.html#a37f16a335f7a3ac65f83e3545c3e50c"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_finRingType</span> := <a class="idref" href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11"><span class="id" title="notation">finRingType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_finLmodType</span> := <a class="idref" href="mathcomp.algebra.finalg.html#89ed2b9c4fe0e2b73b78eb3dc17a4b6f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#89ed2b9c4fe0e2b73b78eb3dc17a4b6f"><span class="id" title="notation">finLmodType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#89ed2b9c4fe0e2b73b78eb3dc17a4b6f"><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#89ed2b9c4fe0e2b73b78eb3dc17a4b6f"><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#006f6a476eaf49ff2271764c2e9c0634"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#006f6a476eaf49ff2271764c2e9c0634"><span class="id" title="notation">finLalgType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#006f6a476eaf49ff2271764c2e9c0634"><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#006f6a476eaf49ff2271764c2e9c0634"><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#e1046e375fa30252214f407945285be1"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#e1046e375fa30252214f407945285be1"><span class="id" title="notation">finAlgType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#e1046e375fa30252214f407945285be1"><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#e1046e375fa30252214f407945285be1"><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/>
+<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#9926250b7ba3fd427de487631b06d875"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.abelian.html#9926250b7ba3fd427de487631b06d875"><span class="id" title="notation">abelem</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">]</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="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/>
+<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#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="abbreviation">R</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">]</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="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/>
+<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#228e85e3c31a939cba019f255574c875"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="mathcomp.ssreflect.eqtype.html#228e85e3c31a939cba019f255574c875"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#09508509373ff3217fbbadb14d25dc5c"><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#09508509373ff3217fbbadb14d25dc5c"><span class="id" title="notation">]</span></a>%<span class="id" title="var">g</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="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/>
+<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#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><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/>
+<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#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.field.finfield.html#PrimeChar.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><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/>
+<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#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.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/>
+<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#6d9094556d4642bd9374f6c3dcaee079"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.vector.html#6d9094556d4642bd9374f6c3dcaee079"><span class="id" title="notation">dim</span></a> <a class="idref" href="mathcomp.algebra.vector.html#6a45c77a68f1019c1f3b35b71c415ac8"><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#6a45c77a68f1019c1f3b35b71c415ac8"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.finalg.html#157b0761db3726d8e1bc0a71108dc48f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#157b0761db3726d8e1bc0a71108dc48f"><span class="id" title="notation">finUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#157b0761db3726d8e1bc0a71108dc48f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.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#157b0761db3726d8e1bc0a71108dc48f"><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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.finalg.html#2aaa42abe766947d0080d3fd1521c4bc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#2aaa42abe766947d0080d3fd1521c4bc"><span class="id" title="notation">finUnitAlgType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#2aaa42abe766947d0080d3fd1521c4bc"><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#2aaa42abe766947d0080d3fd1521c4bc"><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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.field.falgebra.html#8fcc6f073a7a36fa680d6889440e6651"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.field.falgebra.html#8fcc6f073a7a36fa680d6889440e6651"><span class="id" title="notation">FalgType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8fcc6f073a7a36fa680d6889440e6651"><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#8fcc6f073a7a36fa680d6889440e6651"><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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.finalg.html#b13c97e55bebdc1c181a99b80106c099"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#b13c97e55bebdc1c181a99b80106c099"><span class="id" title="notation">finComRingType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#b13c97e55bebdc1c181a99b80106c099"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.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#b13c97e55bebdc1c181a99b80106c099"><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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.finalg.html#29c2dac4b2cace3201f3f23b551d143a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#29c2dac4b2cace3201f3f23b551d143a"><span class="id" title="notation">finComUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#29c2dac4b2cace3201f3f23b551d143a"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.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#29c2dac4b2cace3201f3f23b551d143a"><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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.finalg.html#762465ada9848b70124d860dd97a755c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#762465ada9848b70124d860dd97a755c"><span class="id" title="notation">finIdomainType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#762465ada9848b70124d860dd97a755c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.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#762465ada9848b70124d860dd97a755c"><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/>
+<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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.finfield.html#F0"><span class="id" title="variable">F0</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">]</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">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/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_finFieldType</span> := <a class="idref" href="mathcomp.algebra.finalg.html#85a9f33cca8b2a31e30517c43d5ecb47"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#85a9f33cca8b2a31e30517c43d5ecb47"><span class="id" title="notation">finFieldType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#85a9f33cca8b2a31e30517c43d5ecb47"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.finfield.html#F"><span class="id" title="abbreviation">F</span></a><a class="idref" href="mathcomp.algebra.finalg.html#85a9f33cca8b2a31e30517c43d5ecb47"><span class="id" title="notation">]</span></a>.<br/>
 </div>
 
 <div class="doc">
@@ -354,8 +353,8 @@
  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/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_fieldExtType</span> := <a class="idref" href="mathcomp.field.fieldext.html#78069a19fdca27731326a2758b55293c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.field.fieldext.html#78069a19fdca27731326a2758b55293c"><span class="id" title="notation">fieldExtType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.field.fieldext.html#78069a19fdca27731326a2758b55293c"><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#78069a19fdca27731326a2758b55293c"><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#78069a19fdca27731326a2758b55293c"><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#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.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/>
@@ -377,37 +376,37 @@
  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/>
+<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#95065d7eff417cb87497b35ad25bda41"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.vector.html#95065d7eff417cb87497b35ad25bda41"><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#95065d7eff417cb87497b35ad25bda41"><span class="id" title="notation">}</span></a>) := (<a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.field.finfield.html#FinSplittingField.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.vector.html#6d9094556d4642bd9374f6c3dcaee079"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.vector.html#6d9094556d4642bd9374f6c3dcaee079"><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/>
+<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#810f00798e9fd6a59691271bacabea40"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.field.fieldext.html#810f00798e9fd6a59691271bacabea40"><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#810f00798e9fd6a59691271bacabea40"><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/>
+<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#6a45c77a68f1019c1f3b35b71c415ac8"><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#6a45c77a68f1019c1f3b35b71c415ac8"><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/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">{</span></a><span class="id" title="var">alpha</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><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#1f007a2c34bca981c8e1e44634ce1d47"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.galois.html#1f007a2c34bca981c8e1e44634ce1d47"><span class="id" title="notation">Gal</span></a><a class="idref" href="mathcomp.field.galois.html#1f007a2c34bca981c8e1e44634ce1d47"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.vector.html#6a45c77a68f1019c1f3b35b71c415ac8"><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#6a45c77a68f1019c1f3b35b71c415ac8"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.field.galois.html#1f007a2c34bca981c8e1e44634ce1d47"><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#1f007a2c34bca981c8e1e44634ce1d47"><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/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#663140372ac3b275aae871b74b140513"><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/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><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/>
+<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#65f0b8f4dcd5cfd6280e7c777466601a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/>
+&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#65f0b8f4dcd5cfd6280e7c777466601a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/>
+&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">{</span></a><span class="id" title="var">alpha</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><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#1f007a2c34bca981c8e1e44634ce1d47"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.galois.html#1f007a2c34bca981c8e1e44634ce1d47"><span class="id" title="notation">Gal</span></a><a class="idref" href="mathcomp.field.galois.html#1f007a2c34bca981c8e1e44634ce1d47"><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#1f007a2c34bca981c8e1e44634ce1d47"><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#1f007a2c34bca981c8e1e44634ce1d47"><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/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#663140372ac3b275aae871b74b140513"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><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/>
+<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#810f00798e9fd6a59691271bacabea40"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.field.fieldext.html#810f00798e9fd6a59691271bacabea40"><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#810f00798e9fd6a59691271bacabea40"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.finfield.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.finfield.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#663140372ac3b275aae871b74b140513"><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#df45e8c2e8370fd4f0f7c4fdaf208180"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/>
@@ -438,15 +437,15 @@
 </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/>
+&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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.field.finfield.html#F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.field.finfield.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><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/>
+<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#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.field.finfield.html#F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><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#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">{</span></a><span class="id" title="var">L</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.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/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><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#387983a03fdf688b74a29beb3a4344bb"><span class="id" title="notation">^%:</span></a><a class="idref" href="mathcomp.field.finfield.html#387983a03fdf688b74a29beb3a4344bb"><span class="id" title="notation">A</span></a> <a class="idref" href="mathcomp.algebra.vector.html#6a45c77a68f1019c1f3b35b71c415ac8"><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#6a45c77a68f1019c1f3b35b71c415ac8"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">}</span></a>.<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/>
+<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#81fd94e251a61ee523cdd7855774ae7c"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> 0 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">{</span></a><span class="id" title="var">Fm</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><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/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.finfield.html#Fm"><span class="id" title="variable">Fm</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.finfield.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><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/>
@@ -466,7 +465,7 @@
 <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/>
+<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#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.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/>
@@ -478,7 +477,7 @@
  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/>
+<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/V8.9.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#3609d85e23333c9e68741ad96b416eec"><span class="id" title="notation">*%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#3609d85e23333c9e68741ad96b416eec"><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/>
@@ -488,12 +487,12 @@
 &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/>
+&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>.<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/>
+<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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><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/>
+&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.field.galois.html#205eef6999e87a23b5f8f5c2e8fec9d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.field.galois.html#205eef6999e87a23b5f8f5c2e8fec9d8"><span class="id" title="notation">splittingFieldType</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#3867d54b9d705d180f2100b53dccbd0a"><span class="id" title="notation">F_p</span></a> <a class="idref" href="mathcomp.field.galois.html#205eef6999e87a23b5f8f5c2e8fec9d8"><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#205eef6999e87a23b5f8f5c2e8fec9d8"><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#205eef6999e87a23b5f8f5c2e8fec9d8"><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/>
author	Enrico Tassi	2019-05-22 13:43:08 +0200
committer	Enrico Tassi	2019-05-22 15:34:14 +0200
commit	748d716efb2f2f75946c8386e441ce1789806a39 (patch)
tree	fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/mathcomp.field.finfield.html
parent	415be3b908daadabf178a292c885db78e5b2c9a4 (diff)