diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.field.finfield.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.field.finfield.html | 509 |
1 files changed, 0 insertions, 509 deletions
diff --git a/docs/htmldoc/mathcomp.field.finfield.html b/docs/htmldoc/mathcomp.field.finfield.html deleted file mode 100644 index 398b5de..0000000 --- a/docs/htmldoc/mathcomp.field.finfield.html +++ /dev/null @@ -1,509 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" -"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.field.finfield</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.field.finfield</h1> - -<div class="code"> -<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> - Distributed under the terms of CeCILL-B. *)</span><br/> - -<br/> -</div> - -<div class="doc"> - Additional constructions and results on finite fields. - -<div class="paragraph"> </div> - - FinFieldExtType L == A FinFieldType structure on the carrier of L, - where L IS a fieldExtType F structure for an - F that has a finFieldType structure. This - does not take any existing finType structure - on L; this should not be made canonical. - FinSplittingFieldType F L == A SplittingFieldType F structure on the - carrier of L, where L IS a fieldExtType F for - an F with a finFieldType structure; this - should not be made canonical. - Import FinVector :: Declares canonical default finType, finRing, - etc structures (including FinFieldExtType - above) for abstract vectType, FalgType and - fieldExtType over a finFieldType. This should - be used with caution (e.g., local to a proof) - as the finType so obtained may clash with the - canonical one for standard types like matrix. - PrimeCharType charRp == The carrier of a ringType R such that - charRp : p \in [char R] holds. This type has - canonical ringType, ..., fieldType structures - compatible with those of R, as well as - canonical lmodType 'F_p, ..., algType 'F_p - structures, plus an FalgType structure if R - is a finUnitRingType and a splittingFieldType - struture if R is a finFieldType. - FinSplittingFieldFor nz_p == sigma-pair whose sval is a splittingFieldType - that is the splitting field for p : {poly F} - over F : finFieldType, given nz_p : p != 0. - PrimePowerField pr_p k_gt0 == sigma2-triple whose s2val is a finFieldType - of characteristic p and order m = p ^ k, - given pr_p : prime p and k_gt0 : k > 0. - FinDomainFieldType domR == A finFieldType structure on a finUnitRingType - R, given domR : GRing.IntegralDomain.axiom R. - This is intended to be used inside proofs, - where one cannot declare Canonical instances. - Otherwise one should construct explicitly the - intermediate structures using the ssralg and - finalg constructors, and finDomain_mulrC domR - finDomain_fieldP domR to prove commutativity - and field axioms (the former is Wedderburn's - little theorem). - FinDomainSplittingFieldType domR charRp == A splittingFieldType structure - that repackages the two constructions above. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> - -<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span> <span class="id" title="var">GRing.Theory</span> <span class="id" title="var">FinRing.Theory</span>.<br/> -<span class="id" title="keyword">Local Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">ring_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="FinRing"><span class="id" title="section">FinRing</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="FinRing.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Ring.Exports.finRingType"><span class="id" title="abbreviation">finRingType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="finRing_nontrivial"><span class="id" title="lemma">finRing_nontrivial</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#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#00fe0eaf5e6949f0a31725357afa4bba"><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#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/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="FinField"><span class="id" title="section">FinField</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="FinField.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Field.Exports.finFieldType"><span class="id" title="abbreviation">finFieldType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="card_finField_unit"><span class="id" title="lemma">card_finField_unit</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#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#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0) :=<br/> - <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#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">:></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#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">:></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/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">&</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#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#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/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="CardVspace"><span class="id" title="section">CardVspace</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="CardVspace.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Field.Exports.finFieldType"><span class="id" title="abbreviation">finFieldType</span></a>) (<a name="CardVspace.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="CardVspace.Vector"><span class="id" title="section">Vector</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="CardVspace.Vector.cvT"><span class="id" title="variable">cvT</span></a> : <a class="idref" href="mathcomp.algebra.vector.html#Vector.class_of"><span class="id" title="record">Vector.class_of</span></a> <a class="idref" href="mathcomp.field.finfield.html#CardVspace.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.field.finfield.html#CardVspace.T"><span class="id" title="variable">T</span></a>.<br/> -<span class="id" title="keyword">Let</span> <a name="CardVspace.Vector.vT"><span class="id" title="variable">vT</span></a> := <a class="idref" href="mathcomp.algebra.vector.html#Vector.Pack"><span class="id" title="constructor">Vector.Pack</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/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#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#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/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#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/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="VectFinMixin"><span class="id" title="lemma">VectFinMixin</span></a> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Ring.Exports.finRingType"><span class="id" title="abbreviation">finRingType</span></a>) (<span class="id" title="var">vT</span> : <a class="idref" href="mathcomp.algebra.vector.html#Vector.Exports.vectType"><span class="id" title="abbreviation">vectType</span></a> <a class="idref" href="mathcomp.field.finfield.html#R"><span class="id" title="variable">R</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.mixin_of"><span class="id" title="record">Finite.mixin_of</span></a> <a class="idref" href="mathcomp.field.finfield.html#vT"><span class="id" title="variable">vT</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - These instancces are not exported by default because they conflict with - existing finType instances such as matrix_finType or primeChar_finType. -</div> -<div class="code"> -<span class="id" title="keyword">Module</span> <a name="FinVector"><span class="id" title="module">FinVector</span></a>.<br/> -<span class="id" title="keyword">Section</span> <a name="FinVector.Interfaces"><span class="id" title="section">Interfaces</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="FinVector.Interfaces.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Field.Exports.finFieldType"><span class="id" title="abbreviation">finFieldType</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">vT</span> : <a class="idref" href="mathcomp.algebra.vector.html#Vector.Exports.vectType"><span class="id" title="abbreviation">vectType</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinVector.Interfaces.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">aT</span> : <a class="idref" href="mathcomp.field.falgebra.html#Falgebra.Exports.FalgType"><span class="id" title="abbreviation">FalgType</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinVector.Interfaces.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">fT</span> : <a class="idref" href="mathcomp.field.fieldext.html#FieldExt.Exports.fieldExtType"><span class="id" title="abbreviation">fieldExtType</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinVector.Interfaces.F"><span class="id" title="variable">F</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">vect_finType</span> <span class="id" title="var">vT</span> := <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinType"><span class="id" title="abbreviation">FinType</span></a> <a class="idref" href="mathcomp.field.finfield.html#vT"><span class="id" title="variable">vT</span></a> (<a class="idref" href="mathcomp.field.finfield.html#VectFinMixin"><span class="id" title="lemma">VectFinMixin</span></a> <a class="idref" href="mathcomp.field.finfield.html#vT"><span class="id" title="variable">vT</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Falg_finType</span> <span class="id" title="var">aT</span> := <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinType"><span class="id" title="abbreviation">FinType</span></a> <a class="idref" href="mathcomp.field.finfield.html#aT"><span class="id" title="variable">aT</span></a> (<a class="idref" href="mathcomp.field.finfield.html#VectFinMixin"><span class="id" title="lemma">VectFinMixin</span></a> <a class="idref" href="mathcomp.field.finfield.html#aT"><span class="id" title="variable">aT</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fieldExt_finType</span> <span class="id" title="var">fT</span> := <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinType"><span class="id" title="abbreviation">FinType</span></a> <a class="idref" href="mathcomp.field.finfield.html#fT"><span class="id" title="variable">fT</span></a> (<a class="idref" href="mathcomp.field.finfield.html#VectFinMixin"><span class="id" title="lemma">VectFinMixin</span></a> <a class="idref" href="mathcomp.field.finfield.html#fT"><span class="id" title="variable">fT</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Falg_finRingType</span> <span class="id" title="var">aT</span> := <a class="idref" href="mathcomp.algebra.finalg.html#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/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#FinVector.Interfaces"><span class="id" title="section">Interfaces</span></a>.<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#FinVector"><span class="id" title="module">FinVector</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="FinFieldExtType"><span class="id" title="abbreviation">FinFieldExtType</span></a> := <a class="idref" href="mathcomp.field.finfield.html#fieldExt_finFieldType"><span class="id" title="definition">FinVector.fieldExt_finFieldType</span></a>.<br/> -<span class="id" title="keyword">Notation</span> <a name="FinSplittingFieldAxiom"><span class="id" title="abbreviation">FinSplittingFieldAxiom</span></a> := (<a class="idref" href="mathcomp.field.finfield.html#finField_splittingField_axiom"><span class="id" title="lemma">FinVector.finField_splittingField_axiom</span></a> <span class="id" title="var">_</span>).<br/> -<span class="id" title="keyword">Notation</span> <a name="FinSplittingFieldType"><span class="id" title="abbreviation">FinSplittingFieldType</span></a> <span class="id" title="var">F</span> <span class="id" title="var">L</span> :=<br/> - (<a class="idref" href="mathcomp.field.galois.html#SplittingField.Exports.SplittingFieldType"><span class="id" title="abbreviation">SplittingFieldType</span></a> <span class="id" title="var">F</span> <span class="id" title="var">L</span> <a class="idref" href="mathcomp.field.finfield.html#FinSplittingFieldAxiom"><span class="id" title="abbreviation">FinSplittingFieldAxiom</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="PrimeChar"><span class="id" title="section">PrimeChar</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="PrimeChar.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/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/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="PrimeChar.PrimeCharRing.R0"><span class="id" title="variable">R0</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="PrimeCharType"><span class="id" title="definition">PrimeCharType</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/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/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#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#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#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">:></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#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/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/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/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/> - <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/> - <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#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#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#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/> - -<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_unitRingType</span> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.UnitRing.Exports.unitRingType"><span class="id" title="abbreviation">unitRingType</span></a>) <span class="id" title="var">charRp</span> :=<br/> - <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/> - <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/> - <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/> - <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/> - <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/> - <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/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#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#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#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#228e85e3c31a939cba019f255574c875"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="mathcomp.ssreflect.eqtype.html#228e85e3c31a939cba019f255574c875"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.field.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#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#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#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#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/> - <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/> - <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/> - <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/> - <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/> - <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/> - <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/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#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"> - We need to use the eta-long version of the constructor here as projections - of the Canonical fieldType of F cannot be computed syntactically. -</div> -<div class="code"> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">primeChar_fieldExtType</span> := <a class="idref" href="mathcomp.field.fieldext.html#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/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.finfield.html#PrimeChar"><span class="id" title="section">PrimeChar</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="FinSplittingField"><span class="id" title="section">FinSplittingField</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="FinSplittingField.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.Field.Exports.finFieldType"><span class="id" title="abbreviation">finFieldType</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - By card_vspace order K = #|K| for any finType structure on L; however we - do not want to impose the FinVector instance here. -</div> -<div class="code"> -<span class="id" title="keyword">Let</span> <a name="FinSplittingField.order"><span class="id" title="variable">order</span></a> (<span class="id" title="var">L</span> : <a class="idref" href="mathcomp.algebra.vector.html#Vector.Exports.vectType"><span class="id" title="abbreviation">vectType</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinSplittingField.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">K</span> : <a class="idref" href="mathcomp.algebra.vector.html#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#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#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/> - <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">&</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#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/> - (<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/> - <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/> - <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="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#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/> - <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/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="FinFieldExists"><span class="id" title="section">FinFieldExists</span></a>.<br/> -</div> - -<div class="doc"> - While he existence of finite splitting fields and of finite fields of - arbitrary prime power order is mathematically straightforward, it is - technically challenging to formalize in Coq. The Coq typechecker performs - poorly for the spme of the deeply nested dependent types used in the - construction, such as polynomials over extensions of extensions of finite - fields. Any conversion in a nested structure parameter incurs a huge - overhead as it is shared across term comparison by call-by-need evalution. - The proof of FinSplittingFieldFor is contrived to mitigate this effect: - the abbreviation map_poly_extField alone divides by 3 the proof checking - time, by reducing the number of occurrences of field(Ext)Type structures - in the subgoals; the succesive, apparently redundant 'suffices' localize - some of the conversions to smaller subgoals, yielding a further 8-fold - time gain. In particular, we construct the splitting field as a subtype - of a recursive construction rather than prove that the latter yields - precisely a splitting field. -<div class="paragraph"> </div> - - The apparently redundant type annotation reduces checking time by 30%. -</div> -<div class="code"> -<span class="id" title="keyword">Let</span> <a name="FinFieldExists.map_poly_extField"><span class="id" title="variable">map_poly_extField</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.fieldType"><span class="id" title="abbreviation">fieldType</span></a>) (<span class="id" title="var">L</span> : <a class="idref" href="mathcomp.field.fieldext.html#FieldExt.Exports.fieldExtType"><span class="id" title="abbreviation">fieldExtType</span></a> <a class="idref" href="mathcomp.field.finfield.html#F"><span class="id" title="variable">F</span></a>) :=<br/> - <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#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/> - <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#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/> - <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"><</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">&</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/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="FinDomain"><span class="id" title="section">FinDomain</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">ssrnum</span> <span class="id" title="var">ssrint</span> <span class="id" title="var">algC</span> <span class="id" title="var">cyclotomic</span> <span class="id" title="var">Num.Theory</span>.<br/> -<span class="comment">(* Hide polynomial divisibility. *)</span><br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="FinDomain.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.UnitRing.Exports.finUnitRingType"><span class="id" title="abbreviation">finUnitRingType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Hypothesis</span> <a name="FinDomain.domR"><span class="id" title="variable">domR</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.axiom"><span class="id" title="definition">GRing.IntegralDomain.axiom</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Let</span> <a name="FinDomain.lregR"><span class="id" title="variable">lregR</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.field.finfield.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#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/> - -<br/> -</div> - -<div class="doc"> - This is Witt's proof of Wedderburn's little theorem. -</div> -<div class="code"> -<span class="id" title="keyword">Theorem</span> <a name="finDomain_mulrC"><span class="id" title="lemma">finDomain_mulrC</span></a> : @<a class="idref" href="http://coq.inria.fr/distrib/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/> - <span class="id" title="keyword">let</span> <span class="id" title="var">fin_unit_class</span> := <a class="idref" href="mathcomp.algebra.finalg.html#FinRing.UnitRing.class"><span class="id" title="definition">FinRing.UnitRing.class</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a> <span class="id" title="tactic">in</span><br/> - <span class="id" title="keyword">let</span> <span class="id" title="var">com_class</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ComRing.Class"><span class="id" title="constructor">GRing.ComRing.Class</span></a> <a class="idref" href="mathcomp.field.finfield.html#finDomain_mulrC"><span class="id" title="lemma">finDomain_mulrC</span></a> <span class="id" title="tactic">in</span><br/> - <span class="id" title="keyword">let</span> <span class="id" title="var">com_unit_class</span> := @<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ComUnitRing.Class"><span class="id" title="constructor">GRing.ComUnitRing.Class</span></a> <a class="idref" href="mathcomp.field.finfield.html#FinDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.field.finfield.html#com_class"><span class="id" title="variable">com_class</span></a> <a class="idref" href="mathcomp.field.finfield.html#fin_unit_class"><span class="id" title="variable">fin_unit_class</span></a> <span class="id" title="tactic">in</span><br/> - <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/> - <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/> - <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/> - <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/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/> - <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/> - <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/> -</div> -</div> - -<div id="footer"> -<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> -</div> - -</div> - -</body> -</html>
\ No newline at end of file |