diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.field.algnum.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.field.algnum.html | 451 |
1 files changed, 451 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.field.algnum.html b/docs/htmldoc/mathcomp.field.algnum.html new file mode 100644 index 0000000..ea7733e --- /dev/null +++ b/docs/htmldoc/mathcomp.field.algnum.html @@ -0,0 +1,451 @@ +<!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/> +<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + 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> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.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>).<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/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">{</span></a><span class="id" title="var">z</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">a</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#cd1bca6dfdb74a6b15c6c8969f27472a"><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/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#b2bfc5b99c28e2c89b336d5f86347706"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b2bfc5b99c28e2c89b336d5f86347706"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b2bfc5b99c28e2c89b336d5f86347706"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.algebra.ssralg.html#b2bfc5b99c28e2c89b336d5f86347706"><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#b2bfc5b99c28e2c89b336d5f86347706"><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#9625b440a0052f6dbfd015f5bb8b5125"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9625b440a0052f6dbfd015f5bb8b5125"><span class="id" title="notation">_i</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#891e51846c7d1d63a9cb5458374cf308"><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/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">ps</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#b7adbae1ad6b5f8e6d4ef64ae286f319"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#b7adbae1ad6b5f8e6d4ef64ae286f319"><span class="id" title="notation">seq</span></a> <a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><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#9956cd3926e9966aa6979e465e39d037"><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#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#b7adbae1ad6b5f8e6d4ef64ae286f319"><span class="id" title="notation">|</span></a> <span class="id" title="var">p</span> <a class="idref" href="mathcomp.ssreflect.seq.html#b7adbae1ad6b5f8e6d4ef64ae286f319"><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#b7adbae1ad6b5f8e6d4ef64ae286f319"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">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#bdb1eed686184a9a4099efa772be7bc7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#bdb1eed686184a9a4099efa772be7bc7"><span class="id" title="notation">unitAlgType</span></a> <a class="idref" href="mathcomp.field.algnum.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#bdb1eed686184a9a4099efa772be7bc7"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.field.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#bdb1eed686184a9a4099efa772be7bc7"><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/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">{</span></a><span class="id" title="var">Qs</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><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/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">{</span></a><span class="id" title="var">QsC</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">}</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">{</span></a><span class="id" title="var">s1</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.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/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.field.falgebra.html#e4ccb61d3c0d4e7e716fb926f4a43f39"><span class="id" title="notation"><<</span></a>1 <a class="idref" href="mathcomp.field.falgebra.html#e4ccb61d3c0d4e7e716fb926f4a43f39"><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#e4ccb61d3c0d4e7e716fb926f4a43f39"><span class="id" title="notation">>></span></a>%<span class="id" title="var">VS</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><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/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><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#cd1bca6dfdb74a6b15c6c8969f27472a"><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/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#640778742e86daa97d31c9911c679af3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#640778742e86daa97d31c9911c679af3"><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#22058a36a53dac65c94ca403bc62650a"><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#9625b440a0052f6dbfd015f5bb8b5125"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9625b440a0052f6dbfd015f5bb8b5125"><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/8.8.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/8.8.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/8.8.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.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/8.8.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/8.8.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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#d54beaee78833d410cb3b1b3603748cc"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d54beaee78833d410cb3b1b3603748cc"><span class="id" title="notation">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.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/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><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#81f8078534dcbb7e13a32d292f766525"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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#22058a36a53dac65c94ca403bc62650a"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.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#22058a36a53dac65c94ca403bc62650a"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#208bc995000a6307bdbc043c43919d97"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#208bc995000a6307bdbc043c43919d97"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#208bc995000a6307bdbc043c43919d97"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#208bc995000a6307bdbc043c43919d97"><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#22058a36a53dac65c94ca403bc62650a"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#208bc995000a6307bdbc043c43919d97"><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/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">{</span></a><span class="id" title="var">CtoQn</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.field.algnum.html#CtoQn"><span class="id" title="variable">CtoQn</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.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/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">y</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">{</span></a><span class="id" title="var">nu0</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2759afce9315ab3f51737bc14cc79ce9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2759afce9315ab3f51737bc14cc79ce9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#2759afce9315ab3f51737bc14cc79ce9"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><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/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><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/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><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/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">}</span></a>)(<span class="id" title="var">nu</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">{</span></a><span class="id" title="var">nu0</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2759afce9315ab3f51737bc14cc79ce9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2759afce9315ab3f51737bc14cc79ce9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#2759afce9315ab3f51737bc14cc79ce9"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><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/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><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/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><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/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +</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#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><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/8.8.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/8.8.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#b7adbae1ad6b5f8e6d4ef64ae286f319"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#b7adbae1ad6b5f8e6d4ef64ae286f319"><span class="id" title="notation">seq</span></a> <a class="idref" href="mathcomp.algebra.matrix.html#5cbf3f9f063e1ee805c433f40b533623"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.matrix.html#5cbf3f9f063e1ee805c433f40b533623"><span class="id" title="notation">row_</span></a><a class="idref" href="mathcomp.algebra.matrix.html#5cbf3f9f063e1ee805c433f40b533623"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.algebra.matrix.html#5cbf3f9f063e1ee805c433f40b533623"><span class="id" title="notation"><</span></a> 1<a class="idref" href="mathcomp.algebra.matrix.html#5cbf3f9f063e1ee805c433f40b533623"><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#b7adbae1ad6b5f8e6d4ef64ae286f319"><span class="id" title="notation">|</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.seq.html#b7adbae1ad6b5f8e6d4ef64ae286f319"><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#b7adbae1ad6b5f8e6d4ef64ae286f319"><span class="id" title="notation">]</span></a>) (<a class="idref" href="mathcomp.algebra.matrix.html#cf6654c80d96ae2da5730746e8dfeac4"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.matrix.html#cf6654c80d96ae2da5730746e8dfeac4"><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/8.8.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/8.8.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#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><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/8.8.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">phi</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">{</span></a><span class="id" title="var">nu</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><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/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><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/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><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/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +</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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">{</span></a><span class="id" title="var">u</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">|</span></a> <span class="id" title="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#fb22424322c3d7eb9b837dfca65ce21e"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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#fb22424322c3d7eb9b837dfca65ce21e"><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/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred_class"><span class="id" title="abbreviation">pred_class</span></a> :=<br/> + <span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> : <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.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><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/8.8.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/8.8.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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#e6408d45e92e642f7d1652448339ba09"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#e6408d45e92e642f7d1652448339ba09"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.Crat"><span class="id" title="definition">Crat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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#626a4f68393e32b84ab75f15f785f640"><span class="id" title="notation">%:~</span></a><a class="idref" href="mathcomp.algebra.ssrint.html#626a4f68393e32b84ab75f15f785f640"><span class="id" title="notation">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.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>.<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#19ab5cfd7e4f60fa14f22b576013bd96"><span class="id" title="notation">></span></a> 0)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algnum.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.algebra.poly.html#da242fdb489aa84109b1eed313339a83"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.algebra.poly.html#da242fdb489aa84109b1eed313339a83"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.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#92efb5ea268b6e2f9a125afe76aecbba"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.algebra.poly.html#92efb5ea268b6e2f9a125afe76aecbba"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><span class="id" title="notation">{</span></a><span class="id" title="var">S</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.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/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><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/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <span class="comment">(*b*)</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">}</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><span class="id" title="notation">&</span></a> <span class="comment">(*c*)</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><span class="id" title="notation">{</span></a><span class="id" title="var">Y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">{</span></a><span class="id" title="var">n</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><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#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><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/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><span class="id" title="notation">&</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">}</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><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/8.8.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.ssreflect.eqtype.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#S"><span class="id" title="variable">S</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><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#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#S"><span class="id" title="variable">S</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">}</span></a>) <span class="id" title="var">x</span> :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred_class"><span class="id" title="abbreviation">pred_class</span></a> :=<br/> + <span class="id" title="keyword">fun</span> <span class="id" title="var">z</span> : <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/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><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#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><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#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><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#4fa85b0aa898c2a7e18c3b076438c2e7"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.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/8.8.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/8.8.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="e7209283e722c6e40e30933ff8c369bf"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.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="7da9af325ee9f6fee0c1bf8c89728243"><span class="id" title="notation">"</span></a>e %| x" := (@<a class="idref" href="http://coq.inria.fr/distrib/8.8.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/8.8.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#7da9af325ee9f6fee0c1bf8c89728243"><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#d70623330b2787db6b196e37db7d8f45"><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="a83b4a4a6a4605f304f23e70f728d425"><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="6b3c2ba2fd1701a980405aa74c483b0c"><span class="id" title="notation">"</span></a>x != y %[mod e ]" := (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><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>.<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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>)%<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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> (<a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> (<a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">==</span></a> 0 <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.algnum.html#7da9af325ee9f6fee0c1bf8c89728243"><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#941c6d086004545bd62614d0213e75e5"><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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><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#ae4d81913e6239182a9ac7467ffde8cd"><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#a83b4a4a6a4605f304f23e70f728d425"><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#ae4d81913e6239182a9ac7467ffde8cd"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><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#ae4d81913e6239182a9ac7467ffde8cd"><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#a83b4a4a6a4605f304f23e70f728d425"><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#ae4d81913e6239182a9ac7467ffde8cd"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.field.algnum.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algnum.html#y1"><span class="id" title="variable">y1</span></a> <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algnum.html#x1"><span class="id" title="variable">x1</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><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#a83b4a4a6a4605f304f23e70f728d425"><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#ae4d81913e6239182a9ac7467ffde8cd"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">==</span></a> 0 <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><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>.<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/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><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#a83b4a4a6a4605f304f23e70f728d425"><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#22058a36a53dac65c94ca403bc62650a"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</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/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algnum.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><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#a83b4a4a6a4605f304f23e70f728d425"><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#22058a36a53dac65c94ca403bc62650a"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</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/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">==</span></a> 0 <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</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/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">==</span></a> 0 <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</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/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <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#22058a36a53dac65c94ca403bc62650a"><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#ae4d81913e6239182a9ac7467ffde8cd"><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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</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/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algnum.html#y1"><span class="id" title="variable">y1</span></a> <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algnum.html#x1"><span class="id" title="variable">x1</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><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#a83b4a4a6a4605f304f23e70f728d425"><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#22058a36a53dac65c94ca403bc62650a"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#0ebfa8e4076fc95e12536d4b6a76aa07"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#0ebfa8e4076fc95e12536d4b6a76aa07"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#0ebfa8e4076fc95e12536d4b6a76aa07"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#0ebfa8e4076fc95e12536d4b6a76aa07"><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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.field.algnum.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.field.algC.html#ad6c1a2e0c593edef8f546c6caff1370"><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#ad6c1a2e0c593edef8f546c6caff1370"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algC.html#ad6c1a2e0c593edef8f546c6caff1370"><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#ad6c1a2e0c593edef8f546c6caff1370"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">C</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#0ebfa8e4076fc95e12536d4b6a76aa07"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">==</span></a> 0 <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.algC.html#9a2f23320469c9d2a314bb86625d5b32"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><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/8.8.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#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.field.algnum.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#29294f431c8c9e3d170b3ccfa621d03f"><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#29294f431c8c9e3d170b3ccfa621d03f"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.div.html#29294f431c8c9e3d170b3ccfa621d03f"><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#29294f431c8c9e3d170b3ccfa621d03f"><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/8.8.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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">==</span></a> 0 <a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.field.algnum.html#a83b4a4a6a4605f304f23e70f728d425"><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#a83b4a4a6a4605f304f23e70f728d425"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.field.algnum.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><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/8.8.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#2f8e234f25a0bfb63d8d9325ebea52f2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#2f8e234f25a0bfb63d8d9325ebea52f2"><span class="id" title="notation">pick</span></a> <span class="id" title="var">n</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#2f8e234f25a0bfb63d8d9325ebea52f2"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">(</span></a>2 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><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#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> 2<a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#2f8e234f25a0bfb63d8d9325ebea52f2"><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#17d28d004d0863cb022d4ce832ddaaae"><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#84e794f5513e5917c9e68cdf3e4a2b12"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.cyclotomic.html#84e794f5513e5917c9e68cdf3e4a2b12"><span class="id" title="notation">Phi_n</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#2f8e234f25a0bfb63d8d9325ebea52f2"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="9e3cbdcf44a196e2f90e9ad446025ea4"><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#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.field.algnum.html#9e3cbdcf44a196e2f90e9ad446025ea4"><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#9e3cbdcf44a196e2f90e9ad446025ea4"><span class="id" title="notation">]</span></a>%<span class="id" title="var">C</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 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#9e3cbdcf44a196e2f90e9ad446025ea4"><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#9e3cbdcf44a196e2f90e9ad446025ea4"><span class="id" title="notation">]</span></a>%<span class="id" title="var">C</span> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.algnum.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.field.algnum.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/> +</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 |