diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.field.algnum.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.field.algnum.html | 449 |
1 files changed, 0 insertions, 449 deletions
diff --git a/docs/htmldoc/mathcomp.field.algnum.html b/docs/htmldoc/mathcomp.field.algnum.html deleted file mode 100644 index fe44530..0000000 --- a/docs/htmldoc/mathcomp.field.algnum.html +++ /dev/null @@ -1,449 +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.algnum</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.field.algnum</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"> - This file provides a few basic results and constructions in algebraic - number theory, that are used in the character theory library. Most of - these could be generalized to a more abstract setting. Note that the type - of abstract number fields is simply extFieldType rat. We define here: - x \in Crat_span X <=> x is a Q-linear combination of elements of - X : seq algC. - x \in Cint_span X <=> x is a Z-linear combination of elements of - X : seq algC. - x \in Aint <=> x : algC is an algebraic integer, i.e., the (monic) - polynomial of x over Q has integer coeficients. - (e %| a)%A <=> e divides a with respect to algebraic integers, - (e %| a)%Ax i.e., a is in the algebraic integer ideal generated - by e. This is is notation for a \in dvdA e, where - dvdv is the (collective) predicate for the Aint - ideal generated by e. As in the (e %| a)%C notation - e and a can be coerced to algC from nat or int. - The (e %| a)%Ax display form is a workaround for - design limitations of the Coq Notation facilities. - (a == b % [mod e])%A, (a != b % [mod e])%A <=> - a is equal (resp. not equal) to b mod e, i.e., a and - b belong to the same e * Aint class. We do not - force a, b and e to be algebraic integers. - # [x]%C == the multiplicative order of x, i.e., the n such that - x is an nth primitive root of unity, or 0 if x is not - a root of unity. - In addition several lemmas prove the (constructive) existence of number - fields and of automorphisms of algC. -</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">GRing.Theory</span> <span class="id" title="var">Num.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/> - -<br/> - -<br/> -<span class="id" title="keyword">Local Hint Resolve</span> (<a class="idref" href="mathcomp.algebra.ssrint.html#intr_inj"><span class="id" title="definition">intr_inj</span></a> <a class="idref" href="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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> <a class="idref" href="mathcomp.field.algnum.html#ZtoC"><span class="id" title="abbreviation">ZtoC</span></a>) : <span class="id" title="var">core</span>.<br/> - -<br/> -</div> - -<div class="doc"> - Number fields and rational spans. -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="algC_PET"><span class="id" title="lemma">algC_PET</span></a> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</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">z</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">a</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#c93a2e1bb8503fc4a9598804b268d1be"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#784f0af919f467115774be372bf0dbd7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#784f0af919f467115774be372bf0dbd7"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#784f0af919f467115774be372bf0dbd7"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.algebra.ssralg.html#784f0af919f467115774be372bf0dbd7"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#784f0af919f467115774be372bf0dbd7"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">_i</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#e9001f602764f7896bb1eb34bf606a23"><span class="id" title="notation">*+</span></a> <a class="idref" href="mathcomp.field.algnum.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.field.algnum.html#i"><span class="id" title="variable">i</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.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">ps</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</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.seq.html#dcd18413b33436252c77b6c6465f02bc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#dcd18413b33436252c77b6c6465f02bc"><span class="id" title="notation">seq</span></a> <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.algnum.html#pQtoC"><span class="id" title="abbreviation">pQtoC</span></a> <a class="idref" href="mathcomp.field.algnum.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#dcd18413b33436252c77b6c6465f02bc"><span class="id" title="notation">|</span></a> <span class="id" title="var">p</span> <a class="idref" href="mathcomp.ssreflect.seq.html#dcd18413b33436252c77b6c6465f02bc"><span class="id" title="notation"><-</span></a> <a class="idref" href="mathcomp.field.algnum.html#ps"><span class="id" title="variable">ps</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#dcd18413b33436252c77b6c6465f02bc"><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">Canonical</span> <span class="id" title="var">subfx_unitAlgType</span> (<span class="id" title="var">F</span> <span class="id" title="var">L</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="keyword">iota</span> (<span class="id" title="var">z</span> : <a class="idref" href="mathcomp.field.algnum.html#L"><span class="id" title="variable">L</span></a>) <span class="id" title="var">p</span> :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#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.field.algnum.html#F"><span class="id" title="variable">F</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.fieldext.html#subFExtend"><span class="id" title="definition">subFExtend</span></a> <a class="idref" href="mathcomp.field.algnum.html#iota"><span class="id" title="variable">iota</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.algnum.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#53130370ad22aac4f3ee8434dbc4850d"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="num_field_exists"><span class="id" title="lemma">num_field_exists</span></a> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a>) :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">{</span></a><span class="id" title="var">Qs</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.fieldext.html#FieldExt.Exports.fieldExtType"><span class="id" title="abbreviation">fieldExtType</span></a> <a class="idref" href="mathcomp.algebra.rat.html#rat"><span class="id" title="record">rat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">{</span></a><span class="id" title="var">QsC</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.algnum.html#Qs"><span class="id" title="variable">Qs</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><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#cc5e56ba3765e2d6b17e66d19b966f1d"><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">s1</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.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.algnum.html#Qs"><span class="id" title="variable">Qs</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.seq.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="mathcomp.field.algnum.html#QsC"><span class="id" title="variable">QsC</span></a> <a class="idref" href="mathcomp.field.algnum.html#s1"><span class="id" title="variable">s1</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.algnum.html#s"><span class="id" title="variable">s</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.falgebra.html#371fc5178e74e35fccdd110881a97487"><span class="id" title="notation"><<</span></a>1 <a class="idref" href="mathcomp.field.falgebra.html#371fc5178e74e35fccdd110881a97487"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.field.algnum.html#s1"><span class="id" title="variable">s1</span></a><a class="idref" href="mathcomp.field.falgebra.html#371fc5178e74e35fccdd110881a97487"><span class="id" title="notation">>></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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.vector.html#fullv"><span class="id" title="definition">fullv</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">}}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="in_Crat_span"><span class="id" title="definition">in_Crat_span</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> :=<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">a</span> : <a class="idref" href="mathcomp.algebra.rat.html#rat"><span class="id" title="record">rat</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#c93a2e1bb8503fc4a9598804b268d1be"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#de3e30c288f66ee879ea2b40e81e186c"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#de3e30c288f66ee879ea2b40e81e186c"><span class="id" title="notation">sum_i</span></a> <a class="idref" href="mathcomp.field.algnum.html#QtoC"><span class="id" title="abbreviation">QtoC</span></a> (<a class="idref" href="mathcomp.field.algnum.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.field.algnum.html#i"><span class="id" title="variable">i</span></a>) <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">_i</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Fact</span> <a name="Crat_span_subproof"><span class="id" title="lemma">Crat_span_subproof</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#decidable"><span class="id" title="definition">decidable</span></a> (<a class="idref" href="mathcomp.field.algnum.html#in_Crat_span"><span class="id" title="definition">in_Crat_span</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Crat_span"><span class="id" title="definition">Crat_span</span></a> <span class="id" title="var">s</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a> := <a class="idref" href="mathcomp.field.algnum.html#Crat_span_subproof"><span class="id" title="lemma">Crat_span_subproof</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a>.<br/> -<span class="id" title="keyword">Lemma</span> <a name="Crat_spanP"><span class="id" title="lemma">Crat_spanP</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.field.algnum.html#in_Crat_span"><span class="id" title="definition">in_Crat_span</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Crat_span"><span class="id" title="definition">Crat_span</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a>).<br/> - <span class="id" title="keyword">Fact</span> <a name="Crat_span_key"><span class="id" title="lemma">Crat_span_key</span></a> <span class="id" title="var">s</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred_key"><span class="id" title="inductive">pred_key</span></a> (<a class="idref" href="mathcomp.field.algnum.html#Crat_span"><span class="id" title="definition">Crat_span</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a>). <br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Crat_span_keyed</span> <span class="id" title="var">s</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#KeyedPred"><span class="id" title="definition">KeyedPred</span></a> (<a class="idref" href="mathcomp.field.algnum.html#Crat_span_key"><span class="id" title="lemma">Crat_span_key</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="mem_Crat_span"><span class="id" title="lemma">mem_Crat_span</span></a> <span class="id" title="var">s</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.algnum.html#Crat_span"><span class="id" title="definition">Crat_span</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Fact</span> <a name="Crat_span_zmod_closed"><span class="id" title="lemma">Crat_span_zmod_closed</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.zmod_closed"><span class="id" title="abbreviation">zmod_closed</span></a> (<a class="idref" href="mathcomp.field.algnum.html#Crat_span"><span class="id" title="definition">Crat_span</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Crat_span_opprPred</span> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.OpprPred"><span class="id" title="definition">OpprPred</span></a> (<a class="idref" href="mathcomp.field.algnum.html#Crat_span_zmod_closed"><span class="id" title="lemma">Crat_span_zmod_closed</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Crat_span_addrPred</span> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.AddrPred"><span class="id" title="definition">AddrPred</span></a> (<a class="idref" href="mathcomp.field.algnum.html#Crat_span_zmod_closed"><span class="id" title="lemma">Crat_span_zmod_closed</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Crat_span_zmodPred</span> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.ZmodPred"><span class="id" title="definition">ZmodPred</span></a> (<a class="idref" href="mathcomp.field.algnum.html#Crat_span_zmod_closed"><span class="id" title="lemma">Crat_span_zmod_closed</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="MoreAlgCaut"><span class="id" title="section">MoreAlgCaut</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">rR</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.UnitRing.Exports.unitRingType"><span class="id" title="abbreviation">unitRingType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="alg_num_field"><span class="id" title="lemma">alg_num_field</span></a> (<span class="id" title="var">Qz</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.algebra.rat.html#rat"><span class="id" title="record">rat</span></a>) <span class="id" title="var">a</span> : <a class="idref" href="mathcomp.field.algnum.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#862982ed16052c855fd1cdb6c8e69ea7"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#862982ed16052c855fd1cdb6c8e69ea7"><span class="id" title="notation">A</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.rat.html#ratr"><span class="id" title="definition">ratr</span></a> <a class="idref" href="mathcomp.field.algnum.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#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.field.algnum.html#Qz"><span class="id" title="variable">Qz</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="rmorphZ_num"><span class="id" title="lemma">rmorphZ_num</span></a> (<span class="id" title="var">Qz</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.algebra.rat.html#rat"><span class="id" title="record">rat</span></a>) <span class="id" title="var">rR</span> (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.algnum.html#Qz"><span class="id" title="variable">Qz</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.algnum.html#rR"><span class="id" title="variable">rR</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">}</span></a>) <span class="id" title="var">a</span> <span class="id" title="var">x</span> :<br/> - <a class="idref" href="mathcomp.field.algnum.html#f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.field.algnum.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#3b05480e39db306e67fadbc79d394529"><span class="id" title="notation">*:</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.rat.html#ratr"><span class="id" title="definition">ratr</span></a> <a class="idref" href="mathcomp.field.algnum.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.algnum.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="fmorph_numZ"><span class="id" title="lemma">fmorph_numZ</span></a> (<span class="id" title="var">Qz1</span> <span class="id" title="var">Qz2</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.algebra.rat.html#rat"><span class="id" title="record">rat</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.algnum.html#Qz1"><span class="id" title="variable">Qz1</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.algnum.html#Qz2"><span class="id" title="variable">Qz2</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Linear.Exports.scalable"><span class="id" title="abbreviation">scalable</span></a> <a class="idref" href="mathcomp.field.algnum.html#f"><span class="id" title="variable">f</span></a>.<br/> - <span class="id" title="keyword">Definition</span> <a name="NumLRmorphism"><span class="id" title="definition">NumLRmorphism</span></a> <span class="id" title="var">Qz1</span> <span class="id" title="var">Qz2</span> <span class="id" title="var">f</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.LRMorphism.Exports.AddLRMorphism"><span class="id" title="abbreviation">AddLRMorphism</span></a> (@<a class="idref" href="mathcomp.field.algnum.html#fmorph_numZ"><span class="id" title="lemma">fmorph_numZ</span></a> <a class="idref" href="mathcomp.field.algnum.html#Qz1"><span class="id" title="variable">Qz1</span></a> <a class="idref" href="mathcomp.field.algnum.html#Qz2"><span class="id" title="variable">Qz2</span></a> <a class="idref" href="mathcomp.field.algnum.html#f"><span class="id" title="variable">f</span></a>).<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.algnum.html#MoreAlgCaut"><span class="id" title="section">MoreAlgCaut</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="NumFieldProj"><span class="id" title="section">NumFieldProj</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="NumFieldProj.Qn"><span class="id" title="variable">Qn</span></a> : <a class="idref" href="mathcomp.field.fieldext.html#FieldExt.Exports.fieldExtType"><span class="id" title="abbreviation">fieldExtType</span></a> <a class="idref" href="mathcomp.algebra.rat.html#rat"><span class="id" title="record">rat</span></a>) (<a name="NumFieldProj.QnC"><span class="id" title="variable">QnC</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.algnum.html#Qn"><span class="id" title="variable">Qn</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">}</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Crat_spanZ"><span class="id" title="lemma">Crat_spanZ</span></a> <span class="id" title="var">b</span> <span class="id" title="var">a</span> : <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.algnum.html#Crat_span"><span class="id" title="definition">Crat_span</span></a> <a class="idref" href="mathcomp.field.algnum.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.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.algebra.rat.html#ratr"><span class="id" title="definition">ratr</span></a> <a class="idref" href="mathcomp.field.algnum.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.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Crat_span"><span class="id" title="definition">Crat_span</span></a> <a class="idref" href="mathcomp.field.algnum.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.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Crat_spanM"><span class="id" title="lemma">Crat_spanM</span></a> <span class="id" title="var">b</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.Crat"><span class="id" title="definition">Crat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.field.algnum.html#Crat_span"><span class="id" title="definition">Crat_span</span></a> <a class="idref" href="mathcomp.field.algnum.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.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">a</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.field.algnum.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.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Crat_span"><span class="id" title="definition">Crat_span</span></a> <a class="idref" href="mathcomp.field.algnum.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.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - In principle CtoQn could be taken to be additive and Q-linear, but this - would require a limit construction. -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="num_field_proj"><span class="id" title="lemma">num_field_proj</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">CtoQn</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.field.algnum.html#CtoQn"><span class="id" title="variable">CtoQn</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.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.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.field.algnum.html#NumFieldProj.QnC"><span class="id" title="variable">QnC</span></a> <a class="idref" href="mathcomp.field.algnum.html#CtoQn"><span class="id" title="variable">CtoQn</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="restrict_aut_to_num_field"><span class="id" title="lemma">restrict_aut_to_num_field</span></a> (<span class="id" title="var">nu</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">}</span></a>) :<br/> - <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><span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">y</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.algnum.html#nu"><span class="id" title="variable">nu</span></a> (<a class="idref" href="mathcomp.field.algnum.html#NumFieldProj.QnC"><span class="id" title="variable">QnC</span></a> <a class="idref" href="mathcomp.field.algnum.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.algnum.html#NumFieldProj.QnC"><span class="id" title="variable">QnC</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</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.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#6556914db359db999889decec6a4a562"><span class="id" title="notation">{</span></a><span class="id" title="var">nu0</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.algebra.ssralg.html#c998d6ecd14e902f7fd2311ac585dfed"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#c998d6ecd14e902f7fd2311ac585dfed"><span class="id" title="notation">lrmorphism</span></a> <a class="idref" href="mathcomp.field.algnum.html#NumFieldProj.Qn"><span class="id" title="variable">Qn</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.algnum.html#NumFieldProj.Qn"><span class="id" title="variable">Qn</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#c998d6ecd14e902f7fd2311ac585dfed"><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> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.field.algnum.html#NumFieldProj.QnC"><span class="id" title="variable">QnC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">:</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#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.field.algnum.html#nu0"><span class="id" title="variable">nu0</span></a> <a class="idref" href="mathcomp.field.algnum.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#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.field.algnum.html#nu"><span class="id" title="variable">nu</span></a> <a class="idref" href="mathcomp.field.algnum.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#8bf6fdbe8b0c22b67e58fa5cd9937190"><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="map_Qnum_poly"><span class="id" title="lemma">map_Qnum_poly</span></a> (<span class="id" title="var">nu</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">}</span></a>) <span class="id" title="var">p</span> :<br/> - <a class="idref" href="mathcomp.field.algnum.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.poly.html#polyOver"><span class="id" title="definition">polyOver</span></a> 1%<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.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> (<a class="idref" href="mathcomp.field.algnum.html#nu"><span class="id" title="variable">nu</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.field.algnum.html#NumFieldProj.QnC"><span class="id" title="variable">QnC</span></a>) <a class="idref" href="mathcomp.field.algnum.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#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.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.field.algnum.html#NumFieldProj.QnC"><span class="id" title="variable">QnC</span></a> <a class="idref" href="mathcomp.field.algnum.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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.algnum.html#NumFieldProj"><span class="id" title="section">NumFieldProj</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="restrict_aut_to_normal_num_field"><span class="id" title="lemma">restrict_aut_to_normal_num_field</span></a> (<span class="id" title="var">Qn</span> : <a class="idref" href="mathcomp.field.galois.html#SplittingField.Exports.splittingFieldType"><span class="id" title="abbreviation">splittingFieldType</span></a> <a class="idref" href="mathcomp.algebra.rat.html#rat"><span class="id" title="record">rat</span></a>)<br/> - (<span class="id" title="var">QnC</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.algnum.html#Qn"><span class="id" title="variable">Qn</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">}</span></a>)(<span class="id" title="var">nu</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><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#6556914db359db999889decec6a4a562"><span class="id" title="notation">{</span></a><span class="id" title="var">nu0</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.algebra.ssralg.html#c998d6ecd14e902f7fd2311ac585dfed"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#c998d6ecd14e902f7fd2311ac585dfed"><span class="id" title="notation">lrmorphism</span></a> <a class="idref" href="mathcomp.field.algnum.html#Qn"><span class="id" title="variable">Qn</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.algnum.html#Qn"><span class="id" title="variable">Qn</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#c998d6ecd14e902f7fd2311ac585dfed"><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> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.field.algnum.html#QnC"><span class="id" title="variable">QnC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">:</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#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.field.algnum.html#nu0"><span class="id" title="variable">nu0</span></a> <a class="idref" href="mathcomp.field.algnum.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#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.field.algnum.html#nu"><span class="id" title="variable">nu</span></a> <a class="idref" href="mathcomp.field.algnum.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#8bf6fdbe8b0c22b67e58fa5cd9937190"><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/> -</div> - -<div class="doc"> - Integral spans. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="dec_Cint_span"><span class="id" title="lemma">dec_Cint_span</span></a> (<span class="id" title="var">V</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.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a>) <span class="id" title="var">m</span> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.field.algnum.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.field.algnum.html#V"><span class="id" title="variable">V</span></a>) <span class="id" title="var">v</span> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#decidable"><span class="id" title="definition">decidable</span></a> (<a class="idref" href="mathcomp.algebra.intdiv.html#inIntSpan"><span class="id" title="definition">inIntSpan</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.field.algnum.html#v"><span class="id" title="variable">v</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Cint_span"><span class="id" title="definition">Cint_span</span></a> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a> :=<br/> - <span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.field.algnum.html#dec_Cint_span"><span class="id" title="lemma">dec_Cint_span</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#in_tuple"><span class="id" title="definition">in_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#dcd18413b33436252c77b6c6465f02bc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#dcd18413b33436252c77b6c6465f02bc"><span class="id" title="notation">seq</span></a> <a class="idref" href="mathcomp.algebra.matrix.html#e008ec0beb9d729fd1ef8df8b1024615"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.matrix.html#e008ec0beb9d729fd1ef8df8b1024615"><span class="id" title="notation">row_</span></a><a class="idref" href="mathcomp.algebra.matrix.html#e008ec0beb9d729fd1ef8df8b1024615"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.algebra.matrix.html#e008ec0beb9d729fd1ef8df8b1024615"><span class="id" title="notation"><</span></a> 1<a class="idref" href="mathcomp.algebra.matrix.html#e008ec0beb9d729fd1ef8df8b1024615"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#dcd18413b33436252c77b6c6465f02bc"><span class="id" title="notation">|</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.seq.html#dcd18413b33436252c77b6c6465f02bc"><span class="id" title="notation"><-</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#dcd18413b33436252c77b6c6465f02bc"><span class="id" title="notation">]</span></a>) (<a class="idref" href="mathcomp.algebra.matrix.html#e96cc16a4a892792949f73b0ccf32cf1"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.matrix.html#e96cc16a4a892792949f73b0ccf32cf1"><span class="id" title="notation">row_i</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a>).<br/> -<span class="id" title="keyword">Fact</span> <a name="Cint_span_key"><span class="id" title="lemma">Cint_span_key</span></a> <span class="id" title="var">s</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred_key"><span class="id" title="inductive">pred_key</span></a> (<a class="idref" href="mathcomp.field.algnum.html#Cint_span"><span class="id" title="definition">Cint_span</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a>). <br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Cint_span_keyed</span> <span class="id" title="var">s</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#KeyedPred"><span class="id" title="definition">KeyedPred</span></a> (<a class="idref" href="mathcomp.field.algnum.html#Cint_span_key"><span class="id" title="lemma">Cint_span_key</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Cint_spanP"><span class="id" title="lemma">Cint_spanP</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.field.algnum.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a>) <span class="id" title="var">x</span> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.algebra.intdiv.html#inIntSpan"><span class="id" title="definition">inIntSpan</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Cint_span"><span class="id" title="definition">Cint_span</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="mem_Cint_span"><span class="id" title="lemma">mem_Cint_span</span></a> <span class="id" title="var">s</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.algnum.html#Cint_span"><span class="id" title="definition">Cint_span</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Cint_span_zmod_closed"><span class="id" title="lemma">Cint_span_zmod_closed</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.zmod_closed"><span class="id" title="abbreviation">zmod_closed</span></a> (<a class="idref" href="mathcomp.field.algnum.html#Cint_span"><span class="id" title="definition">Cint_span</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Cint_span_opprPred</span> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.OpprPred"><span class="id" title="definition">OpprPred</span></a> (<a class="idref" href="mathcomp.field.algnum.html#Cint_span_zmod_closed"><span class="id" title="lemma">Cint_span_zmod_closed</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Cint_span_addrPred</span> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.AddrPred"><span class="id" title="definition">AddrPred</span></a> (<a class="idref" href="mathcomp.field.algnum.html#Cint_span_zmod_closed"><span class="id" title="lemma">Cint_span_zmod_closed</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Cint_span_zmodPred</span> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.ZmodPred"><span class="id" title="definition">ZmodPred</span></a> (<a class="idref" href="mathcomp.field.algnum.html#Cint_span_zmod_closed"><span class="id" title="lemma">Cint_span_zmod_closed</span></a> <a class="idref" href="mathcomp.field.algnum.html#s"><span class="id" title="variable">s</span></a>).<br/> - -<br/> -</div> - -<div class="doc"> - Automorphism extensions. -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="extend_algC_subfield_aut"><span class="id" title="lemma">extend_algC_subfield_aut</span></a> (<span class="id" title="var">Qs</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.algebra.rat.html#rat"><span class="id" title="record">rat</span></a>)<br/> - (<span class="id" title="var">QsC</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.algnum.html#Qs"><span class="id" title="variable">Qs</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">phi</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.algnum.html#Qs"><span class="id" title="variable">Qs</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.algnum.html#Qs"><span class="id" title="variable">Qs</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><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#6556914db359db999889decec6a4a562"><span class="id" title="notation">{</span></a><span class="id" title="var">nu</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.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><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> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.field.algnum.html#QsC"><span class="id" title="variable">QsC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">:</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#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.field.algnum.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.field.algnum.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#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.field.algnum.html#nu"><span class="id" title="variable">nu</span></a> <a class="idref" href="mathcomp.field.algnum.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#8bf6fdbe8b0c22b67e58fa5cd9937190"><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/> -</div> - -<div class="doc"> - Extended automorphisms of Q_n. -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="Qn_aut_exists"><span class="id" title="lemma">Qn_aut_exists</span></a> <span class="id" title="var">k</span> <span class="id" title="var">n</span> :<br/> - <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.field.algnum.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.algnum.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#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#6556914db359db999889decec6a4a562"><span class="id" title="notation">{</span></a><span class="id" title="var">u</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.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><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="keyword">∀</span> <span class="id" title="var">z</span>, <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#663140372ac3b275aae871b74b140513"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.field.algnum.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algnum.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#663140372ac3b275aae871b74b140513"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.field.algnum.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#6556914db359db999889decec6a4a562"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - Algebraic integers. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Aint"><span class="id" title="definition">Aint</span></a> : <a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">pred</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</span></a> := <span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.minCpoly"><span class="id" title="definition">minCpoly</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">a</span></a> <a class="idref" href="mathcomp.algebra.poly.html#polyOver"><span class="id" title="definition">polyOver</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.Cint"><span class="id" title="definition">Cint</span></a>.<br/> -<span class="id" title="keyword">Fact</span> <a name="Aint_key"><span class="id" title="lemma">Aint_key</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred_key"><span class="id" title="inductive">pred_key</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a>. <br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Aint_keyed</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#KeyedPred"><span class="id" title="definition">KeyedPred</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint_key"><span class="id" title="lemma">Aint_key</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="root_monic_Aint"><span class="id" title="lemma">root_monic_Aint</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> :<br/> - <a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.field.algnum.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algnum.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#c94c2df86ca03f22f8f8b739cd7e1e88"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c94c2df86ca03f22f8f8b739cd7e1e88"><span class="id" title="notation">is</span></a> <a class="idref" href="mathcomp.algebra.poly.html#monic"><span class="id" title="definition">monic</span></a> <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.algnum.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#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">a</span></a> <a class="idref" href="mathcomp.algebra.poly.html#polyOver"><span class="id" title="definition">polyOver</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.Cint"><span class="id" title="definition">Cint</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.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Cint_rat_Aint"><span class="id" title="lemma">Cint_rat_Aint</span></a> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</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.algC.html#Algebraics.Exports.Crat"><span class="id" title="definition">Crat</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.algnum.html#z"><span class="id" title="variable">z</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.algnum.html#Aint"><span class="id" title="definition">Aint</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.algnum.html#z"><span class="id" title="variable">z</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.algC.html#Algebraics.Exports.Cint"><span class="id" title="definition">Cint</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aint_Cint"><span class="id" title="lemma">Aint_Cint</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.Cint"><span class="id" title="definition">Cint</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aint_int"><span class="id" title="lemma">Aint_int</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.ssrint.html#fd24b924079f6f5906ec417190abcf00"><span class="id" title="notation">%:~</span></a><a class="idref" href="mathcomp.algebra.ssrint.html#fd24b924079f6f5906ec417190abcf00"><span class="id" title="notation">R</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.algnum.html#Aint"><span class="id" title="definition">Aint</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aint0"><span class="id" title="lemma">Aint0</span></a> : 0 <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.algnum.html#Aint"><span class="id" title="definition">Aint</span></a>. <br/> -<span class="id" title="keyword">Lemma</span> <a name="Aint1"><span class="id" title="lemma">Aint1</span></a> : 1 <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.algnum.html#Aint"><span class="id" title="definition">Aint</span></a>. <br/> -<span class="id" title="keyword">Hint Resolve</span> <span class="id" title="var">Aint0</span> <span class="id" title="var">Aint1</span> : <span class="id" title="var">core</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aint_unity_root"><span class="id" title="lemma">Aint_unity_root</span></a> <span class="id" title="var">n</span> <span class="id" title="var">x</span> : (<a class="idref" href="mathcomp.field.algnum.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#7f2a7ef2c63af7359b22787a9daf336e"><span class="id" title="notation">></span></a> 0)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algnum.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.algebra.poly.html#acbc7bcbd85a1f81c4f65e93aa5fd967"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.algebra.poly.html#acbc7bcbd85a1f81c4f65e93aa5fd967"><span class="id" title="notation">unity_root</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aint_prim_root"><span class="id" title="lemma">Aint_prim_root</span></a> <span class="id" title="var">n</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.field.algnum.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.algebra.poly.html#ad6a7217bc47606779ec5b6d2378a1dd"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.algebra.poly.html#ad6a7217bc47606779ec5b6d2378a1dd"><span class="id" title="notation">primitive_root</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</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.algnum.html#Aint"><span class="id" title="definition">Aint</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aint_Cnat"><span class="id" title="lemma">Aint_Cnat</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.Cnat"><span class="id" title="definition">Cnat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This is Isaacs, Lemma (3.3) -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="Aint_subring_exists"><span class="id" title="lemma">Aint_subring_exists</span></a> (<span class="id" title="var">X</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a>) :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.field.algnum.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><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><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">{</span></a><span class="id" title="var">S</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">&</span></a><br/> - <span class="comment">(*a*)</span> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.subring_closed"><span class="id" title="abbreviation">subring_closed</span></a> <a class="idref" href="mathcomp.field.algnum.html#S"><span class="id" title="variable">S</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <span class="comment">(*b*)</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.field.algnum.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.algnum.html#S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><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#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">&</span></a> <span class="comment">(*c*)</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">{</span></a><span class="id" title="var">Y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">{</span></a><span class="id" title="var">n</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.field.algnum.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">&</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">subset</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#tagged"><span class="id" title="definition">tagged</span></a> <a class="idref" href="mathcomp.field.algnum.html#Y"><span class="id" title="variable">Y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.algnum.html#S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><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#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">&</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.algebra.intdiv.html#inIntSpan"><span class="id" title="definition">inIntSpan</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#tagged"><span class="id" title="definition">tagged</span></a> <a class="idref" href="mathcomp.field.algnum.html#Y"><span class="id" title="variable">Y</span></a>) <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#S"><span class="id" title="variable">S</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">}}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="AlgIntSubring"><span class="id" title="section">AlgIntSubring</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">DefaultKeying</span> <span class="id" title="var">GRing.DefaultPred</span> <span class="id" title="var">perm</span>.<br/> - -<br/> -</div> - -<div class="doc"> - This is Isaacs, Theorem (3.4). -</div> -<div class="code"> -<span class="id" title="keyword">Theorem</span> <a name="fin_Csubring_Aint"><span class="id" title="lemma">fin_Csubring_Aint</span></a> <span class="id" title="var">S</span> <span class="id" title="var">n</span> (<span class="id" title="var">Y</span> : <a class="idref" href="mathcomp.field.algnum.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a>) :<br/> - <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.mulr_closed"><span class="id" title="abbreviation">mulr_closed</span></a> <a class="idref" href="mathcomp.field.algnum.html#S"><span class="id" title="variable">S</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.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.algebra.intdiv.html#inIntSpan"><span class="id" title="definition">inIntSpan</span></a> <a class="idref" href="mathcomp.field.algnum.html#Y"><span class="id" title="variable">Y</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#S"><span class="id" title="variable">S</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.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.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.field.algnum.html#S"><span class="id" title="variable">S</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This is Isaacs, Corollary (3.5). -</div> -<div class="code"> -<span class="id" title="keyword">Corollary</span> <a name="Aint_subring"><span class="id" title="lemma">Aint_subring</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.subring_closed"><span class="id" title="abbreviation">subring_closed</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Aint_opprPred</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.OpprPred"><span class="id" title="definition">OpprPred</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint_subring"><span class="id" title="lemma">Aint_subring</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Aint_addrPred</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.AddrPred"><span class="id" title="definition">AddrPred</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint_subring"><span class="id" title="lemma">Aint_subring</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Aint_mulrPred</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.MulrPred"><span class="id" title="definition">MulrPred</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint_subring"><span class="id" title="lemma">Aint_subring</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Aint_zmodPred</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.ZmodPred"><span class="id" title="definition">ZmodPred</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint_subring"><span class="id" title="lemma">Aint_subring</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Aint_semiringPred</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.SemiringPred"><span class="id" title="definition">SemiringPred</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint_subring"><span class="id" title="lemma">Aint_subring</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Aint_smulrPred</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.SmulrPred"><span class="id" title="definition">SmulrPred</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint_subring"><span class="id" title="lemma">Aint_subring</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Aint_subringPred</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.SubringPred"><span class="id" title="definition">SubringPred</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint_subring"><span class="id" title="lemma">Aint_subring</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.algnum.html#AlgIntSubring"><span class="id" title="section">AlgIntSubring</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aint_aut"><span class="id" title="lemma">Aint_aut</span></a> (<span class="id" title="var">nu</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">}</span></a>) <span class="id" title="var">x</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.algnum.html#nu"><span class="id" title="variable">nu</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</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.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</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">Definition</span> <a name="dvdA"><span class="id" title="definition">dvdA</span></a> (<span class="id" title="var">e</span> : <a class="idref" href="mathcomp.field.algC.html#Algebraics.divisor"><span class="id" title="definition">Algebraics.divisor</span></a>) : <a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">pred</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</span></a> :=<br/> - <span class="id" title="keyword">fun</span> <span class="id" title="var">z</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#69c431a9c94f6f30a655bd7ddb59037b"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.field.algnum.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#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.algnum.html#Aint"><span class="id" title="definition">Aint</span></a>.<br/> -<span class="id" title="keyword">Fact</span> <a name="dvdA_key"><span class="id" title="lemma">dvdA_key</span></a> <span class="id" title="var">e</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred_key"><span class="id" title="inductive">pred_key</span></a> (<a class="idref" href="mathcomp.field.algnum.html#dvdA"><span class="id" title="definition">dvdA</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a>). <br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">dvdA_keyed</span> <span class="id" title="var">e</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#KeyedPred"><span class="id" title="definition">KeyedPred</span></a> (<a class="idref" href="mathcomp.field.algnum.html#dvdA_key"><span class="id" title="lemma">dvdA_key</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a>).<br/> -<span class="id" title="keyword">Delimit</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">algC_scope</span> <span class="id" title="keyword">with</span> <span class="id" title="var">A</span>.<br/> -<span class="id" title="keyword">Delimit</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">algC_expanded_scope</span> <span class="id" title="keyword">with</span> <span class="id" title="var">Ax</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="122fcad4ef80dc9e0b35edcb2125d6d9"><span class="id" title="notation">"</span></a>e %| x" := (<span class="id" title="var">x</span> <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.algnum.html#dvdA"><span class="id" title="definition">dvdA</span></a> <span class="id" title="var">e</span>) : <span class="id" title="var">algC_expanded_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="0860ab6177cf2be7674499be94490166"><span class="id" title="notation">"</span></a>e %| x" := (@<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#in_mem"><span class="id" title="definition">in_mem</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.divisor"><span class="id" title="definition">Algebraics.divisor</span></a> <span class="id" title="var">x</span> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> (<a class="idref" href="mathcomp.field.algnum.html#dvdA"><span class="id" title="definition">dvdA</span></a> <span class="id" title="var">e</span>))) : <span class="id" title="var">algC_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Fact</span> <a name="dvdA_zmod_closed"><span class="id" title="lemma">dvdA_zmod_closed</span></a> <span class="id" title="var">e</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.zmod_closed"><span class="id" title="abbreviation">zmod_closed</span></a> (<a class="idref" href="mathcomp.field.algnum.html#dvdA"><span class="id" title="definition">dvdA</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">dvdA_opprPred</span> <span class="id" title="var">e</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.OpprPred"><span class="id" title="definition">OpprPred</span></a> (<a class="idref" href="mathcomp.field.algnum.html#dvdA_zmod_closed"><span class="id" title="lemma">dvdA_zmod_closed</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">dvdA_addrPred</span> <span class="id" title="var">e</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.AddrPred"><span class="id" title="definition">AddrPred</span></a> (<a class="idref" href="mathcomp.field.algnum.html#dvdA_zmod_closed"><span class="id" title="lemma">dvdA_zmod_closed</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">dvdA_zmodPred</span> <span class="id" title="var">e</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.ZmodPred"><span class="id" title="definition">ZmodPred</span></a> (<a class="idref" href="mathcomp.field.algnum.html#dvdA_zmod_closed"><span class="id" title="lemma">dvdA_zmod_closed</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="eqAmod"><span class="id" title="definition">eqAmod</span></a> (<span class="id" title="var">e</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.field.algC.html#Algebraics.divisor"><span class="id" title="definition">Algebraics.divisor</span></a>) := (<a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.algnum.html#0860ab6177cf2be7674499be94490166"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">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.algnum.html#y"><span class="id" title="variable">y</span></a>)%<span class="id" title="var">A</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">"</span></a>x == y %[mod e ]" := (<a class="idref" href="mathcomp.field.algnum.html#eqAmod"><span class="id" title="definition">eqAmod</span></a> <span class="id" title="var">e</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">algC_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="ec65dc3af1b511143bc1703d48b82584"><span class="id" title="notation">"</span></a>x != y %[mod e ]" := (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">~~</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.algnum.html#eqAmod"><span class="id" title="definition">eqAmod</span></a> <span class="id" title="var">e</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">)</span></a>) : <span class="id" title="var">algC_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmod_refl"><span class="id" title="lemma">eqAmod_refl</span></a> <span class="id" title="var">e</span> <span class="id" title="var">x</span> : (<a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span>.<br/> - <span class="id" title="keyword">Hint Resolve</span> <span class="id" title="var">eqAmod_refl</span> : <span class="id" title="var">core</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmod_sym"><span class="id" title="lemma">eqAmod_sym</span></a> <span class="id" title="var">e</span> <span class="id" title="var">x</span> <span class="id" title="var">y</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.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><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="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.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><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>)%<span class="id" title="var">A</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmod_trans"><span class="id" title="lemma">eqAmod_trans</span></a> <span class="id" title="var">e</span> <span class="id" title="var">y</span> <span class="id" title="var">x</span> <span class="id" title="var">z</span> :<br/> - (<a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><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.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><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.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmod_transl"><span class="id" title="lemma">eqAmod_transl</span></a> <span class="id" title="var">e</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> :<br/> - (<a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</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.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</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.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmod_transr"><span class="id" title="lemma">eqAmod_transr</span></a> <span class="id" title="var">e</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> :<br/> - (<a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</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.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</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.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmod0"><span class="id" title="lemma">eqAmod0</span></a> <span class="id" title="var">e</span> <span class="id" title="var">x</span> : (<a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> 0 <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</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.algnum.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.algnum.html#0860ab6177cf2be7674499be94490166"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">A</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmodN"><span class="id" title="lemma">eqAmodN</span></a> <span class="id" title="var">e</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : (<a class="idref" href="mathcomp.algebra.ssralg.html#8d0566c961139ec21811f52ef0c317db"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</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.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#8d0566c961139ec21811f52ef0c317db"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmodDr"><span class="id" title="lemma">eqAmodDr</span></a> <span class="id" title="var">e</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : (<a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</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.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmodDl"><span class="id" title="lemma">eqAmodDl</span></a> <span class="id" title="var">e</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : (<a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</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.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmodD"><span class="id" title="lemma">eqAmodD</span></a> <span class="id" title="var">e</span> <span class="id" title="var">x1</span> <span class="id" title="var">x2</span> <span class="id" title="var">y1</span> <span class="id" title="var">y2</span> :<br/> - (<a class="idref" href="mathcomp.field.algnum.html#x1"><span class="id" title="variable">x1</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#x2"><span class="id" title="variable">x2</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><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.field.algnum.html#y1"><span class="id" title="variable">y1</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#y2"><span class="id" title="variable">y2</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><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.field.algnum.html#x1"><span class="id" title="variable">x1</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.algnum.html#y1"><span class="id" title="variable">y1</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#x2"><span class="id" title="variable">x2</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.algnum.html#y2"><span class="id" title="variable">y2</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmodm0"><span class="id" title="lemma">eqAmodm0</span></a> <span class="id" title="var">e</span> : (<a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> 0 <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span>.<br/> - <span class="id" title="keyword">Hint Resolve</span> <span class="id" title="var">eqAmodm0</span> : <span class="id" title="var">core</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmodMr"><span class="id" title="lemma">eqAmodMr</span></a> <span class="id" title="var">e</span> :<br/> - <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.algnum.html#Aint"><span class="id" title="definition">Aint</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">z</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><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.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><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>%<span class="id" title="var">A</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmodMl"><span class="id" title="lemma">eqAmodMl</span></a> <span class="id" title="var">e</span> :<br/> - <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.algnum.html#Aint"><span class="id" title="definition">Aint</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">z</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><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.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><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>%<span class="id" title="var">A</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmodMl0"><span class="id" title="lemma">eqAmodMl0</span></a> <span class="id" title="var">e</span> : <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.algnum.html#Aint"><span class="id" title="definition">Aint</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.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> 0 <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><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>%<span class="id" title="var">A</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmodMr0"><span class="id" title="lemma">eqAmodMr0</span></a> <span class="id" title="var">e</span> : <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.algnum.html#Aint"><span class="id" title="definition">Aint</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.algnum.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> 0 <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><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>%<span class="id" title="var">A</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmod_addl_mul"><span class="id" title="lemma">eqAmod_addl_mul</span></a> <span class="id" title="var">e</span> : <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.algnum.html#Aint"><span class="id" title="definition">Aint</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> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><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>%<span class="id" title="var">A</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmodM"><span class="id" title="lemma">eqAmodM</span></a> <span class="id" title="var">e</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">&,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x1</span> <span class="id" title="var">y2</span> <span class="id" title="var">x2</span> <span class="id" title="var">y1</span>,<br/> - <a class="idref" href="mathcomp.field.algnum.html#x1"><span class="id" title="variable">x1</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#x2"><span class="id" title="variable">x2</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><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.field.algnum.html#y1"><span class="id" title="variable">y1</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#y2"><span class="id" title="variable">y2</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><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.field.algnum.html#x1"><span class="id" title="variable">x1</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.algnum.html#y1"><span class="id" title="variable">y1</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#x2"><span class="id" title="variable">x2</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.algnum.html#y2"><span class="id" title="variable">y2</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">}</span></a>%<span class="id" title="var">A</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmod_rat"><span class="id" title="lemma">eqAmod_rat</span></a> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#41940d7b27ea6f4cfc62b9919ed9d131"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#41940d7b27ea6f4cfc62b9919ed9d131"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.Crat"><span class="id" title="definition">Crat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#41940d7b27ea6f4cfc62b9919ed9d131"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#41940d7b27ea6f4cfc62b9919ed9d131"><span class="id" title="notation">&,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">e</span> <span class="id" title="var">m</span> <span class="id" title="var">n</span>, (<a class="idref" href="mathcomp.field.algnum.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</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.algnum.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.field.algC.html#074a766e3f389a9f57f000217fe90e0f"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.field.algC.html#074a766e3f389a9f57f000217fe90e0f"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algC.html#074a766e3f389a9f57f000217fe90e0f"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algC.html#074a766e3f389a9f57f000217fe90e0f"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">C</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#41940d7b27ea6f4cfc62b9919ed9d131"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmod0_rat"><span class="id" title="lemma">eqAmod0_rat</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.Crat"><span class="id" title="definition">Crat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">&,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">e</span> <span class="id" title="var">n</span>, (<a class="idref" href="mathcomp.field.algnum.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> 0 <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</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.algnum.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.algC.html#a8acd6561c48edf701c07f3c736659e7"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.field.algnum.html#n"><span class="id" title="variable">n</span></a>)%<span class="id" title="var">C</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmod_nat"><span class="id" title="lemma">eqAmod_nat</span></a> (<span class="id" title="var">e</span> <span class="id" title="var">m</span> <span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : (<a class="idref" href="mathcomp.field.algnum.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</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.algnum.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#9c3b63aefc7fc3a3d3aa9b85185d069f"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#9c3b63aefc7fc3a3d3aa9b85185d069f"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.div.html#9c3b63aefc7fc3a3d3aa9b85185d069f"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.ssreflect.div.html#9c3b63aefc7fc3a3d3aa9b85185d069f"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">N</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eqAmod0_nat"><span class="id" title="lemma">eqAmod0_nat</span></a> (<span class="id" title="var">e</span> <span class="id" title="var">m</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : (<a class="idref" href="mathcomp.field.algnum.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">==</span></a> 0 <a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.field.algnum.html#f1011181ef0a006de4cdb60a24b8dc6d"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</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.algnum.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#bde82eab2fe4a0799bc2419e587505d4"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.field.algnum.html#m"><span class="id" title="variable">m</span></a>)%<span class="id" title="var">N</span>.<br/> - -<br/> -</div> - -<div class="doc"> - Multiplicative order. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="orderC"><span class="id" title="definition">orderC</span></a> <span class="id" title="var">x</span> :=<br/> - <span class="id" title="keyword">let</span> <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.minCpoly"><span class="id" title="definition">minCpoly</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="tactic">in</span><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#oapp"><span class="id" title="abbreviation">oapp</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> 0%<span class="id" title="var">N</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#d583921bee6150451237862f0867ac60"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#d583921bee6150451237862f0867ac60"><span class="id" title="notation">pick</span></a> <span class="id" title="var">n</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#d583921bee6150451237862f0867ac60"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">(</span></a>2 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.field.algnum.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> 2<a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#d583921bee6150451237862f0867ac60"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.field.algnum.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.algnum.html#intrp"><span class="id" title="abbreviation">intrp</span></a> <a class="idref" href="mathcomp.field.cyclotomic.html#874b0df808ac9901a8162cab18629aee"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#874b0df808ac9901a8162cab18629aee"><span class="id" title="notation">Phi_n</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#d583921bee6150451237862f0867ac60"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="e0ef1169a0283239169c3e064b6dca4c"><span class="id" title="notation">"</span></a>#[ x ]" := (<a class="idref" href="mathcomp.field.algnum.html#orderC"><span class="id" title="definition">orderC</span></a> <span class="id" title="var">x</span>) : <span class="id" title="var">C_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="exp_orderC"><span class="id" title="lemma">exp_orderC</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.field.algnum.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.algnum.html#e0ef1169a0283239169c3e064b6dca4c"><span class="id" title="notation">#[</span></a><a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.field.algnum.html#e0ef1169a0283239169c3e064b6dca4c"><span class="id" title="notation">]</span></a>%<span class="id" title="var">C</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> 1.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="dvdn_orderC"><span class="id" title="lemma">dvdn_orderC</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</span> : (<a class="idref" href="mathcomp.field.algnum.html#e0ef1169a0283239169c3e064b6dca4c"><span class="id" title="notation">#[</span></a><a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.field.algnum.html#e0ef1169a0283239169c3e064b6dca4c"><span class="id" title="notation">]</span></a>%<span class="id" title="var">C</span> <a class="idref" href="mathcomp.ssreflect.div.html#bde82eab2fe4a0799bc2419e587505d4"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.field.algnum.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#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.algnum.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.algnum.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<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 |