diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.algebra.ring_quotient.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.algebra.ring_quotient.html | 769 |
1 files changed, 769 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.algebra.ring_quotient.html b/docs/htmldoc/mathcomp.algebra.ring_quotient.html new file mode 100644 index 0000000..35d7bc6 --- /dev/null +++ b/docs/htmldoc/mathcomp.algebra.ring_quotient.html @@ -0,0 +1,769 @@ +<!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.algebra.ring_quotient</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library mathcomp.algebra.ring_quotient</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 describes quotients of algebraic structures. + +<div class="paragraph"> </div> + + It defines a join hierarchy mxing the structures defined in file ssralg + (up to unit ring type) and the quotType quotient structure defined in + file generic_quotient. Every structure in that (join) hierarchy is + parametrized by a base type T and the constants and operations on the + base type that will be used to confer its algebraic structure to the + quotient. Note that T itself is in general not an instance of an + algebraic structure. The canonical surjection from T onto its quotient + should be compatible with the parameter operations. + +<div class="paragraph"> </div> + + The second part of the file provides a definition of (non trivial) + decidable ideals (resp. prime ideals) of an arbitrary instance of ring + structure and a construction of the quotient of a ring by such an ideal. + These definitions extend the hierarchy of sub-structures defined in file + ssralg (see Module Pred in ssralg), following a similar methodology. + Although the definition of the (structure of) quotient of a ring by an + ideal is a general one, we do not provide infrastructure for the case of + non commutative ring and left or two-sided ideals. + +<div class="paragraph"> </div> + + The file defines the following Structures: + zmodQuotType T e z n a == Z-module obtained by quotienting type T + with the relation e and whose neutral, + opposite and addition are the images in the + quotient of the parameters z, n and a, + respectively. + ringQuotType T e z n a o m == ring obtained by quotienting type T with + the relation e and whose zero opposite, + addition, one, and multiplication are the + images in the quotient of the parameters + z, n, a, o, m, respectively. + unitRingQuotType ... u i == As in the previous cases, instance of unit + ring whose unit predicate is obtained from + u and the inverse from i. + idealr R S == (S : pred R) is a non-trivial, decidable, + right ideal of the ring R. + prime_idealr R S == (S : pred R) is a non-trivial, decidable, + right, prime ideal of the ring R. + +<div class="paragraph"> </div> + + The formalization of ideals features the following constructions: + proper_ideal S == the collective predicate (S : pred R) on the + ring R is stable by the ring product and does + contain R's one. + prime_idealr_closed S := u * v \in S -> (u \in S) || (v \in S) + idealr_closed S == the collective predicate (S : pred R) on the + ring R represents a (right) ideal. This + implies its being a proper_ideal. + +<div class="paragraph"> </div> + + MkIdeal idealS == packs idealS : proper_ideal S into an + idealr S interface structure associating the + idealr_closed property to the canonical + pred_key S (see ssrbool), which must already + be an zmodPred (see ssralg). + MkPrimeIdeal pidealS == packs pidealS : prime_idealr_closed S into a + prime_idealr S interface structure associating + the prime_idealr_closed property to the + canonical pred_key S (see ssrbool), which must + already be an idealr (see above). + {ideal_quot kI} == quotient by the keyed (right) ideal predicate + kI of a commutative ring R. Note that we indeed + only provide canonical structures of ring + quotients for the case of commutative rings, + for which a right ideal is obviously a + two-sided ideal. + +<div class="paragraph"> </div> + + Note : + if (I : pred R) is a predicate over a ring R and (ideal : idealr I) is an + instance of (right) ideal, in order to quantify over an arbitrary (keyed) + predicate describing ideal, use type (keyed_pred ideal), as in: + forall (kI : keyed_pred ideal),... +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Import</span> <span class="id" title="var">GRing.Theory</span>.<br/> + +<br/> +<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> + +<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/> +<span class="id" title="keyword">Local Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">quotient_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Reserved Notation</span> "{ideal_quot I }" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "{ideal_quot I }").<br/> +<span class="id" title="keyword">Reserved Notation</span> "m = n %[mod_ideal I ]" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">n</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>,<br/> + <span class="id" title="var">format</span> "'[hv ' m '/' = n '/' %[mod_ideal I ] ']'").<br/> +<span class="id" title="keyword">Reserved Notation</span> "m == n %[mod_ideal I ]" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">n</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>,<br/> + <span class="id" title="var">format</span> "'[hv ' m '/' == n '/' %[mod_ideal I ] ']'").<br/> +<span class="id" title="keyword">Reserved Notation</span> "m <> n %[mod_ideal I ]" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">n</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>,<br/> + <span class="id" title="var">format</span> "'[hv ' m '/' <> n '/' %[mod_ideal I ] ']'").<br/> +<span class="id" title="keyword">Reserved Notation</span> "m != n %[mod_ideal I ]" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">n</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>,<br/> + <span class="id" title="var">format</span> "'[hv ' m '/' != n '/' %[mod_ideal I ] ']'").<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="ZmodQuot"><span class="id" title="section">ZmodQuot</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> (<a name="ZmodQuot.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>).<br/> +<span class="id" title="keyword">Variable</span> <a name="ZmodQuot.eqT"><span class="id" title="variable">eqT</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.T"><span class="id" title="variable">T</span></a>.<br/> +<span class="id" title="keyword">Variables</span> (<a name="ZmodQuot.zeroT"><span class="id" title="variable">zeroT</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.T"><span class="id" title="variable">T</span></a>) (<a name="ZmodQuot.oppT"><span class="id" title="variable">oppT</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.T"><span class="id" title="variable">T</span></a>) (<a name="ZmodQuot.addT"><span class="id" title="variable">addT</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.T"><span class="id" title="variable">T</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Record</span> <a name="zmod_quot_mixin_of"><span class="id" title="record">zmod_quot_mixin_of</span></a> (<span class="id" title="var">Q</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">qc</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_class_of"><span class="id" title="abbreviation">quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>)<br/> + (<span class="id" title="var">zc</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.class_of"><span class="id" title="record">GRing.Zmodule.class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>) := <a name="ZmodQuotMixinPack"><span class="id" title="constructor">ZmodQuotMixinPack</span></a> {<br/> + <a name="zmod_eq_quot_mixin"><span class="id" title="projection">zmod_eq_quot_mixin</span></a> :> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_mixin_of"><span class="id" title="definition">eq_quot_mixin_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.eqT"><span class="id" title="variable">eqT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zc"><span class="id" title="variable">zc</span></a>;<br/> + <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypePack"><span class="id" title="constructor">QuotTypePack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.zeroT"><span class="id" title="variable">zeroT</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> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Pack"><span class="id" title="constructor">GRing.Zmodule.Pack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zc"><span class="id" title="variable">zc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>;<br/> + <span class="id" title="var">_</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="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.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypePack"><span class="id" title="constructor">QuotTypePack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><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> <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><br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.oppT"><span class="id" title="variable">oppT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ssralg.html#GRing.opp"><span class="id" title="definition">GRing.opp</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Pack"><span class="id" title="constructor">GRing.Zmodule.Pack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zc"><span class="id" title="variable">zc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.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>;<br/> + <span class="id" title="var">_</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypePack"><span class="id" title="constructor">QuotTypePack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">:</span></a> <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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">/</span></a><br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.addT"><span class="id" title="variable">addT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">>-></span></a> @<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.add"><span class="id" title="definition">GRing.add</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Pack"><span class="id" title="constructor">GRing.Zmodule.Pack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zc"><span class="id" title="variable">zc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">}</span></a><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Record</span> <a name="zmod_quot_class_of"><span class="id" title="record">zmod_quot_class_of</span></a> (<span class="id" title="var">Q</span> : <span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> := <a name="ZmodQuotClass"><span class="id" title="constructor">ZmodQuotClass</span></a> {<br/> + <a name="zmod_quot_quot_class"><span class="id" title="projection">zmod_quot_quot_class</span></a> :> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_class_of"><span class="id" title="abbreviation">quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>;<br/> + <a name="zmod_quot_zmod_class"><span class="id" title="projection">zmod_quot_zmod_class</span></a> :> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.class_of"><span class="id" title="record">GRing.Zmodule.class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>;<br/> + <a name="zmod_quot_mixin"><span class="id" title="projection">zmod_quot_mixin</span></a> :> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_mixin_of"><span class="id" title="record">zmod_quot_mixin_of</span></a><br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_quot_class"><span class="id" title="method">zmod_quot_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_zmod_class"><span class="id" title="method">zmod_quot_zmod_class</span></a><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Structure</span> <a name="zmodQuotType"><span class="id" title="record">zmodQuotType</span></a> : <span class="id" title="keyword">Type</span> := <a name="ZmodQuotTypePack"><span class="id" title="constructor">ZmodQuotTypePack</span></a> {<br/> + <a name="zmod_quot_sort"><span class="id" title="projection">zmod_quot_sort</span></a> :> <span class="id" title="keyword">Type</span>;<br/> + <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class_of"><span class="id" title="record">zmod_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_sort"><span class="id" title="method">zmod_quot_sort</span></a>;<br/> + <span class="id" title="var">_</span> : <span class="id" title="keyword">Type</span><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">zqT</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType"><span class="id" title="record">zmodQuotType</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="zmod_quot_class"><span class="id" title="definition">zmod_quot_class</span></a> <span class="id" title="var">zqT</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class_of"><span class="id" title="record">zmod_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a> :=<br/> + <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuotTypePack"><span class="id" title="constructor">ZmodQuotTypePack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">cT</span> <span class="id" title="var">_</span> <span class="id" title="keyword">as</span> <span class="id" title="var">qT'</span> := <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a> <span class="id" title="keyword">return</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class_of"><span class="id" title="record">zmod_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qT'"><span class="id" title="variable">qT'</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">cT</span>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="zmod_eq_quot_class"><span class="id" title="definition">zmod_eq_quot_class</span></a> <span class="id" title="var">zqT</span> (<span class="id" title="var">zqc</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class_of"><span class="id" title="record">zmod_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a>) :<br/> + <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_class_of"><span class="id" title="record">eq_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.eqT"><span class="id" title="variable">eqT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotClass"><span class="id" title="constructor">EqQuotClass</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqc"><span class="id" title="variable">zqc</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">zmodQuotType_eqType</span> <span class="id" title="var">zqT</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Pack"><span class="id" title="constructor">Equality.Pack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class"><span class="id" title="definition">zmod_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">zmodQuotType_choiceType</span> <span class="id" title="var">zqT</span> :=<br/> + <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Pack"><span class="id" title="constructor">Choice.Pack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class"><span class="id" title="definition">zmod_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">zmodQuotType_zmodType</span> <span class="id" title="var">zqT</span> :=<br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Pack"><span class="id" title="constructor">GRing.Zmodule.Pack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class"><span class="id" title="definition">zmod_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">zmodQuotType_quotType</span> <span class="id" title="var">zqT</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypePack"><span class="id" title="constructor">QuotTypePack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class"><span class="id" title="definition">zmod_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">zmodQuotType_eqQuotType</span> <span class="id" title="var">zqT</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTypePack"><span class="id" title="constructor">EqQuotTypePack</span></a><br/> + (<a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_eq_quot_class"><span class="id" title="definition">zmod_eq_quot_class</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class"><span class="id" title="definition">zmod_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a>)) <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_eqType"><span class="id" title="definition">zmodQuotType_eqType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_eqType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_eqType"><span class="id" title="definition">zmodQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_eqType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_eqType"><span class="id" title="definition">eqType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_choiceType"><span class="id" title="definition">zmodQuotType_choiceType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_choiceType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_choiceType"><span class="id" title="definition">zmodQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_choiceType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_choiceType"><span class="id" title="definition">choiceType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_zmodType"><span class="id" title="definition">zmodQuotType_zmodType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_zmodType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_zmodType"><span class="id" title="definition">zmodQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_zmodType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_zmodType"><span class="id" title="definition">zmodType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_quotType"><span class="id" title="definition">zmodQuotType_quotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_quotType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_quotType"><span class="id" title="definition">zmodQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_quotType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_quotType"><span class="id" title="definition">quotType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_eqQuotType"><span class="id" title="definition">zmodQuotType_eqQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_eqQuotType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_eqQuotType"><span class="id" title="definition">zmodQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_eqQuotType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType_eqQuotType"><span class="id" title="definition">eqQuotType</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="ZmodQuotType_pack"><span class="id" title="definition">ZmodQuotType_pack</span></a> <span class="id" title="var">Q</span> :=<br/> + <span class="id" title="keyword">fun</span> (<span class="id" title="var">qT</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.T"><span class="id" title="variable">T</span></a>) (<span class="id" title="var">zT</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Exports.zmodType"><span class="id" title="abbreviation">zmodType</span></a>) <span class="id" title="var">qc</span> <span class="id" title="var">zc</span><br/> + <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_class"><span class="id" title="projection">quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qT"><span class="id" title="variable">qT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> & <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.class"><span class="id" title="definition">GRing.Zmodule.class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zT"><span class="id" title="variable">zT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#zc"><span class="id" title="variable">zc</span></a> ⇒<br/> + <span class="id" title="keyword">fun</span> <span class="id" title="var">m</span> ⇒ <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuotTypePack"><span class="id" title="constructor">ZmodQuotTypePack</span></a> (@<a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuotClass"><span class="id" title="constructor">ZmodQuotClass</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zc"><span class="id" title="variable">zc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#m"><span class="id" title="variable">m</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="ZmodQuotMixin_pack"><span class="id" title="definition">ZmodQuotMixin_pack</span></a> <span class="id" title="var">Q</span> :=<br/> + <span class="id" title="keyword">fun</span> (<span class="id" title="var">qT</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqQuotType"><span class="id" title="record">eqQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.eqT"><span class="id" title="variable">eqT</span></a>) (<span class="id" title="var">qc</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_class_of"><span class="id" title="record">eq_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.eqT"><span class="id" title="variable">eqT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>)<br/> + <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_class"><span class="id" title="definition">eq_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qT"><span class="id" title="variable">qT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> ⇒<br/> + <span class="id" title="keyword">fun</span> (<span class="id" title="var">zT</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Exports.zmodType"><span class="id" title="abbreviation">zmodType</span></a>) <span class="id" title="var">zc</span> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.class"><span class="id" title="definition">GRing.Zmodule.class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zT"><span class="id" title="variable">zT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#zc"><span class="id" title="variable">zc</span></a> ⇒<br/> + <span class="id" title="keyword">fun</span> <span class="id" title="var">e</span> <span class="id" title="var">m0</span> <span class="id" title="var">mN</span> <span class="id" title="var">mD</span> ⇒ @<a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuotMixinPack"><span class="id" title="constructor">ZmodQuotMixinPack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zc"><span class="id" title="variable">zc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#m0"><span class="id" title="variable">m0</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#mN"><span class="id" title="variable">mN</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#mD"><span class="id" title="variable">mD</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="ZmodQuotType_clone"><span class="id" title="definition">ZmodQuotType_clone</span></a> (<span class="id" title="var">Q</span> : <span class="id" title="keyword">Type</span>) <span class="id" title="var">qT</span> <span class="id" title="var">cT</span><br/> + <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class"><span class="id" title="definition">zmod_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qT"><span class="id" title="variable">qT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#cT"><span class="id" title="variable">cT</span></a> := @<a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuotTypePack"><span class="id" title="constructor">ZmodQuotTypePack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#cT"><span class="id" title="variable">cT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="zmod_quot_mixinP"><span class="id" title="lemma">zmod_quot_mixinP</span></a> <span class="id" title="var">zqT</span> :<br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_mixin_of"><span class="id" title="record">zmod_quot_mixin_of</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class"><span class="id" title="definition">zmod_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a>) (<a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class"><span class="id" title="definition">zmod_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pi_zeror"><span class="id" title="lemma">pi_zeror</span></a> <span class="id" title="var">zqT</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_zqT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.zeroT"><span class="id" title="variable">zeroT</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> 0.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pi_oppr"><span class="id" title="lemma">pi_oppr</span></a> <span class="id" title="var">zqT</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="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.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_zqT</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.algebra.ring_quotient.html#ZmodQuot.oppT"><span class="id" title="variable">oppT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pi_addr"><span class="id" title="lemma">pi_addr</span></a> <span class="id" title="var">zqT</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_zqT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">:</span></a> <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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot.addT"><span class="id" title="variable">addT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ring_quotient.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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_zero_quot_morph</span> <span class="id" title="var">zqT</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiMorph"><span class="id" title="abbreviation">PiMorph</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#pi_zeror"><span class="id" title="lemma">pi_zeror</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a>).<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_opp_quot_morph</span> <span class="id" title="var">zqT</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiMorph1"><span class="id" title="abbreviation">PiMorph1</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#pi_oppr"><span class="id" title="lemma">pi_oppr</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a>).<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_add_quot_morph</span> <span class="id" title="var">zqT</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiMorph2"><span class="id" title="abbreviation">PiMorph2</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#pi_addr"><span class="id" title="lemma">pi_addr</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zqT"><span class="id" title="variable">zqT</span></a>).<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuot"><span class="id" title="section">ZmodQuot</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="ZmodQuotType"><span class="id" title="abbreviation">ZmodQuotType</span></a> <span class="id" title="var">z</span> <span class="id" title="var">o</span> <span class="id" title="var">a</span> <span class="id" title="var">Q</span> <span class="id" title="var">m</span> :=<br/> + (@<a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuotType_pack"><span class="id" title="definition">ZmodQuotType_pack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">z</span> <span class="id" title="var">o</span> <span class="id" title="var">a</span> <span class="id" title="var">Q</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">m</span>).<br/> +<span class="id" title="keyword">Notation</span> <a name="b68f73bafc39ba549c2b0787edb63b18"><span class="id" title="notation">"</span></a>[ 'zmodQuotType' z , o & a 'of' Q ]" :=<br/> + (@<a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuotType_clone"><span class="id" title="definition">ZmodQuotType_clone</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">z</span> <span class="id" title="var">o</span> <span class="id" title="var">a</span> <span class="id" title="var">Q</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'zmodQuotType' z , o & a 'of' Q ]") : <span class="id" title="var">form_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="ZmodQuotMixin"><span class="id" title="abbreviation">ZmodQuotMixin</span></a> <span class="id" title="var">Q</span> <span class="id" title="var">m0</span> <span class="id" title="var">mN</span> <span class="id" title="var">mD</span> :=<br/> + (@<a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuotMixin_pack"><span class="id" title="definition">ZmodQuotMixin_pack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">Q</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#pi_eq_quot"><span class="id" title="lemma">pi_eq_quot</span></a> <span class="id" title="var">_</span>) <span class="id" title="var">m0</span> <span class="id" title="var">mN</span> <span class="id" title="var">mD</span>).<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="PiAdditive"><span class="id" title="section">PiAdditive</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="PiAdditive.V"><span class="id" title="variable">V</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Exports.zmodType"><span class="id" title="abbreviation">zmodType</span></a>) (<a name="PiAdditive.equivV"><span class="id" title="variable">equivV</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#V"><span class="id" title="variable">V</span></a>) (<a name="PiAdditive.zeroV"><span class="id" title="variable">zeroV</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#V"><span class="id" title="variable">V</span></a>).<br/> +<span class="id" title="keyword">Variable</span> <a name="PiAdditive.Q"><span class="id" title="variable">Q</span></a> : @<a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType"><span class="id" title="record">zmodQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#PiAdditive.V"><span class="id" title="variable">V</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#PiAdditive.equivV"><span class="id" title="variable">equivV</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#PiAdditive.zeroV"><span class="id" title="variable">zeroV</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#9fdf1a446ceec36bc97cce801a3ef3f2"><span class="id" title="notation">-%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9fdf1a446ceec36bc97cce801a3ef3f2"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#327bb2f0da6fd7c01a004dedcfc2dee4"><span class="id" title="notation">+%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#327bb2f0da6fd7c01a004dedcfc2dee4"><span class="id" title="notation">R</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pi_is_additive"><span class="id" title="lemma">pi_is_additive</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Additive.Exports.additive"><span class="id" title="abbreviation">additive</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_Q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_additive</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Additive.Exports.Additive"><span class="id" title="abbreviation">Additive</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#pi_is_additive"><span class="id" title="lemma">pi_is_additive</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#PiAdditive"><span class="id" title="section">PiAdditive</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="RingQuot"><span class="id" title="section">RingQuot</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> (<a name="RingQuot.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>).<br/> +<span class="id" title="keyword">Variable</span> <a name="RingQuot.eqT"><span class="id" title="variable">eqT</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.T"><span class="id" title="variable">T</span></a>.<br/> +<span class="id" title="keyword">Variables</span> (<a name="RingQuot.zeroT"><span class="id" title="variable">zeroT</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.T"><span class="id" title="variable">T</span></a>) (<a name="RingQuot.oppT"><span class="id" title="variable">oppT</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.T"><span class="id" title="variable">T</span></a>) (<a name="RingQuot.addT"><span class="id" title="variable">addT</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.T"><span class="id" title="variable">T</span></a>).<br/> +<span class="id" title="keyword">Variables</span> (<a name="RingQuot.oneT"><span class="id" title="variable">oneT</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.T"><span class="id" title="variable">T</span></a>) (<a name="RingQuot.mulT"><span class="id" title="variable">mulT</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.T"><span class="id" title="variable">T</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Record</span> <a name="ring_quot_mixin_of"><span class="id" title="record">ring_quot_mixin_of</span></a> (<span class="id" title="var">Q</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">qc</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_class_of"><span class="id" title="abbreviation">quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>)<br/> + (<span class="id" title="var">rc</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.class_of"><span class="id" title="record">GRing.Ring.class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>) := <a name="RingQuotMixinPack"><span class="id" title="constructor">RingQuotMixinPack</span></a> {<br/> + <a name="ring_zmod_quot_mixin"><span class="id" title="projection">ring_zmod_quot_mixin</span></a> :> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_mixin_of"><span class="id" title="record">zmod_quot_mixin_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.eqT"><span class="id" title="variable">eqT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.zeroT"><span class="id" title="variable">zeroT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.oppT"><span class="id" title="variable">oppT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.addT"><span class="id" title="variable">addT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rc"><span class="id" title="variable">rc</span></a>;<br/> + <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypePack"><span class="id" title="constructor">QuotTypePack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.oneT"><span class="id" title="variable">oneT</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> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Pack"><span class="id" title="constructor">GRing.Ring.Pack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rc"><span class="id" title="variable">rc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>;<br/> + <span class="id" title="var">_</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypePack"><span class="id" title="constructor">QuotTypePack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">:</span></a> <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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">/</span></a><br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.mulT"><span class="id" title="variable">mulT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">>-></span></a> @<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.mul"><span class="id" title="definition">GRing.mul</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Pack"><span class="id" title="constructor">GRing.Ring.Pack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rc"><span class="id" title="variable">rc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">}</span></a><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Record</span> <a name="ring_quot_class_of"><span class="id" title="record">ring_quot_class_of</span></a> (<span class="id" title="var">Q</span> : <span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> := <a name="RingQuotClass"><span class="id" title="constructor">RingQuotClass</span></a> {<br/> + <a name="ring_quot_quot_class"><span class="id" title="projection">ring_quot_quot_class</span></a> :> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_class_of"><span class="id" title="abbreviation">quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>;<br/> + <a name="ring_quot_ring_class"><span class="id" title="projection">ring_quot_ring_class</span></a> :> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.class_of"><span class="id" title="record">GRing.Ring.class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>;<br/> + <a name="ring_quot_mixin"><span class="id" title="projection">ring_quot_mixin</span></a> :> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_mixin_of"><span class="id" title="record">ring_quot_mixin_of</span></a><br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_quot_class"><span class="id" title="method">ring_quot_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_ring_class"><span class="id" title="method">ring_quot_ring_class</span></a><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Structure</span> <a name="ringQuotType"><span class="id" title="record">ringQuotType</span></a> : <span class="id" title="keyword">Type</span> := <a name="RingQuotTypePack"><span class="id" title="constructor">RingQuotTypePack</span></a> {<br/> + <a name="ring_quot_sort"><span class="id" title="projection">ring_quot_sort</span></a> :> <span class="id" title="keyword">Type</span>;<br/> + <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class_of"><span class="id" title="record">ring_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_sort"><span class="id" title="method">ring_quot_sort</span></a>;<br/> + <span class="id" title="var">_</span> : <span class="id" title="keyword">Type</span><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">rqT</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType"><span class="id" title="record">ringQuotType</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="ring_quot_class"><span class="id" title="definition">ring_quot_class</span></a> <span class="id" title="var">rqT</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class_of"><span class="id" title="record">ring_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a> :=<br/> + <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuotTypePack"><span class="id" title="constructor">RingQuotTypePack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">cT</span> <span class="id" title="var">_</span> <span class="id" title="keyword">as</span> <span class="id" title="var">qT'</span> := <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a> <span class="id" title="keyword">return</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class_of"><span class="id" title="record">ring_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qT'"><span class="id" title="variable">qT'</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">cT</span>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="ring_zmod_quot_class"><span class="id" title="definition">ring_zmod_quot_class</span></a> <span class="id" title="var">rqT</span> (<span class="id" title="var">rqc</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class_of"><span class="id" title="record">ring_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) :<br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class_of"><span class="id" title="record">zmod_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.eqT"><span class="id" title="variable">eqT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.zeroT"><span class="id" title="variable">zeroT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.oppT"><span class="id" title="variable">oppT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.addT"><span class="id" title="variable">addT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a> := <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuotClass"><span class="id" title="constructor">ZmodQuotClass</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqc"><span class="id" title="variable">rqc</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="ring_eq_quot_class"><span class="id" title="definition">ring_eq_quot_class</span></a> <span class="id" title="var">rqT</span> (<span class="id" title="var">rqc</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class_of"><span class="id" title="record">ring_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) :<br/> + <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_class_of"><span class="id" title="record">eq_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.eqT"><span class="id" title="variable">eqT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotClass"><span class="id" title="constructor">EqQuotClass</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqc"><span class="id" title="variable">rqc</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ringQuotType_eqType</span> <span class="id" title="var">rqT</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Pack"><span class="id" title="constructor">Equality.Pack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class"><span class="id" title="definition">ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ringQuotType_choiceType</span> <span class="id" title="var">rqT</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Pack"><span class="id" title="constructor">Choice.Pack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class"><span class="id" title="definition">ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ringQuotType_zmodType</span> <span class="id" title="var">rqT</span> :=<br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Pack"><span class="id" title="constructor">GRing.Zmodule.Pack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class"><span class="id" title="definition">ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ringQuotType_ringType</span> <span class="id" title="var">rqT</span> :=<br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Pack"><span class="id" title="constructor">GRing.Ring.Pack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class"><span class="id" title="definition">ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ringQuotType_quotType</span> <span class="id" title="var">rqT</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypePack"><span class="id" title="constructor">QuotTypePack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class"><span class="id" title="definition">ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ringQuotType_eqQuotType</span> <span class="id" title="var">rqT</span> :=<br/> + <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTypePack"><span class="id" title="constructor">EqQuotTypePack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_eq_quot_class"><span class="id" title="definition">ring_eq_quot_class</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class"><span class="id" title="definition">ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>)) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ringQuotType_zmodQuotType</span> <span class="id" title="var">rqT</span> :=<br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuotTypePack"><span class="id" title="constructor">ZmodQuotTypePack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_zmod_quot_class"><span class="id" title="definition">ring_zmod_quot_class</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class"><span class="id" title="definition">ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>)) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_eqType"><span class="id" title="definition">ringQuotType_eqType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_eqType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_eqType"><span class="id" title="definition">ringQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_eqType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_eqType"><span class="id" title="definition">eqType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_choiceType"><span class="id" title="definition">ringQuotType_choiceType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_choiceType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_choiceType"><span class="id" title="definition">ringQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_choiceType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_choiceType"><span class="id" title="definition">choiceType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_zmodType"><span class="id" title="definition">ringQuotType_zmodType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_zmodType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_zmodType"><span class="id" title="definition">ringQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_zmodType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_zmodType"><span class="id" title="definition">zmodType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_ringType"><span class="id" title="definition">ringQuotType_ringType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_ringType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_ringType"><span class="id" title="definition">ringQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_ringType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_ringType"><span class="id" title="definition">ringType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_quotType"><span class="id" title="definition">ringQuotType_quotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_quotType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_quotType"><span class="id" title="definition">ringQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_quotType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_quotType"><span class="id" title="definition">quotType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_eqQuotType"><span class="id" title="definition">ringQuotType_eqQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_eqQuotType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_eqQuotType"><span class="id" title="definition">ringQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_eqQuotType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_eqQuotType"><span class="id" title="definition">eqQuotType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_zmodQuotType"><span class="id" title="definition">ringQuotType_zmodQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_zmodQuotType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_zmodQuotType"><span class="id" title="definition">ringQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_zmodQuotType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType_zmodQuotType"><span class="id" title="definition">zmodQuotType</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="RingQuotType_pack"><span class="id" title="definition">RingQuotType_pack</span></a> <span class="id" title="var">Q</span> :=<br/> + <span class="id" title="keyword">fun</span> (<span class="id" title="var">qT</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.T"><span class="id" title="variable">T</span></a>) (<span class="id" title="var">zT</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</span></a>) <span class="id" title="var">qc</span> <span class="id" title="var">rc</span><br/> + <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_class"><span class="id" title="projection">quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qT"><span class="id" title="variable">qT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> & <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.class"><span class="id" title="definition">GRing.Ring.class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zT"><span class="id" title="variable">zT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rc"><span class="id" title="variable">rc</span></a> ⇒<br/> + <span class="id" title="keyword">fun</span> <span class="id" title="var">m</span> ⇒ <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuotTypePack"><span class="id" title="constructor">RingQuotTypePack</span></a> (@<a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuotClass"><span class="id" title="constructor">RingQuotClass</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rc"><span class="id" title="variable">rc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#m"><span class="id" title="variable">m</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="RingQuotMixin_pack"><span class="id" title="definition">RingQuotMixin_pack</span></a> <span class="id" title="var">Q</span> :=<br/> + <span class="id" title="keyword">fun</span> (<span class="id" title="var">qT</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodQuotType"><span class="id" title="record">zmodQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.eqT"><span class="id" title="variable">eqT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.zeroT"><span class="id" title="variable">zeroT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.oppT"><span class="id" title="variable">oppT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.addT"><span class="id" title="variable">addT</span></a>) ⇒<br/> + <span class="id" title="keyword">fun</span> (<span class="id" title="var">qc</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class_of"><span class="id" title="record">zmod_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.eqT"><span class="id" title="variable">eqT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.zeroT"><span class="id" title="variable">zeroT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.oppT"><span class="id" title="variable">oppT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.addT"><span class="id" title="variable">addT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>)<br/> + <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class"><span class="id" title="definition">zmod_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qT"><span class="id" title="variable">qT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> ⇒<br/> + <span class="id" title="keyword">fun</span> (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</span></a>) <span class="id" title="var">rc</span> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.class"><span class="id" title="definition">GRing.Ring.class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rT"><span class="id" title="variable">rT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rc"><span class="id" title="variable">rc</span></a> ⇒<br/> + <span class="id" title="keyword">fun</span> <span class="id" title="var">mZ</span> <span class="id" title="var">m1</span> <span class="id" title="var">mM</span> ⇒ @<a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuotMixinPack"><span class="id" title="constructor">RingQuotMixinPack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rc"><span class="id" title="variable">rc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#mZ"><span class="id" title="variable">mZ</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#m1"><span class="id" title="variable">m1</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#mM"><span class="id" title="variable">mM</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="RingQuotType_clone"><span class="id" title="definition">RingQuotType_clone</span></a> (<span class="id" title="var">Q</span> : <span class="id" title="keyword">Type</span>) <span class="id" title="var">qT</span> <span class="id" title="var">cT</span><br/> + <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class"><span class="id" title="definition">ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qT"><span class="id" title="variable">qT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#cT"><span class="id" title="variable">cT</span></a> := @<a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuotTypePack"><span class="id" title="constructor">RingQuotTypePack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#cT"><span class="id" title="variable">cT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="ring_quot_mixinP"><span class="id" title="lemma">ring_quot_mixinP</span></a> <span class="id" title="var">rqT</span> :<br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_mixin_of"><span class="id" title="record">ring_quot_mixin_of</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class"><span class="id" title="definition">ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) (<a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class"><span class="id" title="definition">ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pi_oner"><span class="id" title="lemma">pi_oner</span></a> <span class="id" title="var">rqT</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_rqT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.oneT"><span class="id" title="variable">oneT</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.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pi_mulr"><span class="id" title="lemma">pi_mulr</span></a> <span class="id" title="var">rqT</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_rqT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">:</span></a> <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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot.mulT"><span class="id" title="variable">mulT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ring_quotient.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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_one_quot_morph</span> <span class="id" title="var">rqT</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiMorph"><span class="id" title="abbreviation">PiMorph</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#pi_oner"><span class="id" title="lemma">pi_oner</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>).<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_mul_quot_morph</span> <span class="id" title="var">rqT</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiMorph2"><span class="id" title="abbreviation">PiMorph2</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#pi_mulr"><span class="id" title="lemma">pi_mulr</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>).<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuot"><span class="id" title="section">RingQuot</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="RingQuotType"><span class="id" title="abbreviation">RingQuotType</span></a> <span class="id" title="var">o</span> <span class="id" title="var">mul</span> <span class="id" title="var">Q</span> <span class="id" title="var">mix</span> :=<br/> + (@<a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuotType_pack"><span class="id" title="definition">RingQuotType_pack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">o</span> <span class="id" title="var">mul</span> <span class="id" title="var">Q</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">mix</span>).<br/> +<span class="id" title="keyword">Notation</span> <a name="f8690bec8fb96ac4882c6825e7ed98ae"><span class="id" title="notation">"</span></a>[ 'ringQuotType' o & m 'of' Q ]" :=<br/> + (@<a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuotType_clone"><span class="id" title="definition">RingQuotType_clone</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">o</span> <span class="id" title="var">m</span> <span class="id" title="var">Q</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'ringQuotType' o & m 'of' Q ]") : <span class="id" title="var">form_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="RingQuotMixin"><span class="id" title="abbreviation">RingQuotMixin</span></a> <span class="id" title="var">Q</span> <span class="id" title="var">m1</span> <span class="id" title="var">mM</span> :=<br/> + (@<a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuotMixin_pack"><span class="id" title="definition">RingQuotMixin_pack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">Q</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_mixinP"><span class="id" title="lemma">zmod_quot_mixinP</span></a> <span class="id" title="var">_</span>) <span class="id" title="var">m1</span> <span class="id" title="var">mM</span>).<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="PiRMorphism"><span class="id" title="section">PiRMorphism</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="PiRMorphism.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</span></a>) (<a name="PiRMorphism.equivR"><span class="id" title="variable">equivR</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#R"><span class="id" title="variable">R</span></a>) (<a name="PiRMorphism.zeroR"><span class="id" title="variable">zeroR</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#R"><span class="id" title="variable">R</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="PiRMorphism.Q"><span class="id" title="variable">Q</span></a> : @<a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType"><span class="id" title="record">ringQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#PiRMorphism.R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#PiRMorphism.equivR"><span class="id" title="variable">equivR</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#PiRMorphism.zeroR"><span class="id" title="variable">zeroR</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#9fdf1a446ceec36bc97cce801a3ef3f2"><span class="id" title="notation">-%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9fdf1a446ceec36bc97cce801a3ef3f2"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#327bb2f0da6fd7c01a004dedcfc2dee4"><span class="id" title="notation">+%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#327bb2f0da6fd7c01a004dedcfc2dee4"><span class="id" title="notation">R</span></a> 1 <a class="idref" href="mathcomp.algebra.ssralg.html#d5d4e2467843f67554f1a8a22d125de9"><span class="id" title="notation">*%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d5d4e2467843f67554f1a8a22d125de9"><span class="id" title="notation">R</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pi_is_multiplicative"><span class="id" title="lemma">pi_is_multiplicative</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.RMorphism.Exports.multiplicative"><span class="id" title="abbreviation">multiplicative</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_Q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_rmorphism</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.RMorphism.Exports.AddRMorphism"><span class="id" title="abbreviation">AddRMorphism</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#pi_is_multiplicative"><span class="id" title="lemma">pi_is_multiplicative</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#PiRMorphism"><span class="id" title="section">PiRMorphism</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="UnitRingQuot"><span class="id" title="section">UnitRingQuot</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> (<a name="UnitRingQuot.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>).<br/> +<span class="id" title="keyword">Variable</span> <a name="UnitRingQuot.eqT"><span class="id" title="variable">eqT</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a>.<br/> +<span class="id" title="keyword">Variables</span> (<a name="UnitRingQuot.zeroT"><span class="id" title="variable">zeroT</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a>) (<a name="UnitRingQuot.oppT"><span class="id" title="variable">oppT</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a>) (<a name="UnitRingQuot.addT"><span class="id" title="variable">addT</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a>).<br/> +<span class="id" title="keyword">Variables</span> (<a name="UnitRingQuot.oneT"><span class="id" title="variable">oneT</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a>) (<a name="UnitRingQuot.mulT"><span class="id" title="variable">mulT</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a>).<br/> +<span class="id" title="keyword">Variables</span> (<a name="UnitRingQuot.unitT"><span class="id" title="variable">unitT</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.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a>) (<a name="UnitRingQuot.invT"><span class="id" title="variable">invT</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Record</span> <a name="unit_ring_quot_mixin_of"><span class="id" title="record">unit_ring_quot_mixin_of</span></a> (<span class="id" title="var">Q</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">qc</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_class_of"><span class="id" title="abbreviation">quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>)<br/> + (<span class="id" title="var">rc</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.UnitRing.class_of"><span class="id" title="record">GRing.UnitRing.class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>) := <a name="UnitRingQuotMixinPack"><span class="id" title="constructor">UnitRingQuotMixinPack</span></a> {<br/> + <a name="unit_ring_zmod_quot_mixin"><span class="id" title="projection">unit_ring_zmod_quot_mixin</span></a> :><br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_mixin_of"><span class="id" title="record">ring_quot_mixin_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.eqT"><span class="id" title="variable">eqT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.zeroT"><span class="id" title="variable">zeroT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.oppT"><span class="id" title="variable">oppT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.addT"><span class="id" title="variable">addT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.oneT"><span class="id" title="variable">oneT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.mulT"><span class="id" title="variable">mulT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rc"><span class="id" title="variable">rc</span></a>;<br/> + <span class="id" title="var">_</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fcecf6c7c5b99f975a4e95451ce580e5"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fcecf6c7c5b99f975a4e95451ce580e5"><span class="id" title="notation">mono</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypePack"><span class="id" title="constructor">QuotTypePack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fcecf6c7c5b99f975a4e95451ce580e5"><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#fcecf6c7c5b99f975a4e95451ce580e5"><span class="id" title="notation">/</span></a><br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.unitT"><span class="id" title="variable">unitT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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#fcecf6c7c5b99f975a4e95451ce580e5"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ssralg.html#GRing.unit"><span class="id" title="definition">GRing.unit</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.UnitRing.Pack"><span class="id" title="constructor">GRing.UnitRing.Pack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rc"><span class="id" title="variable">rc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fcecf6c7c5b99f975a4e95451ce580e5"><span class="id" title="notation">}</span></a>;<br/> + <span class="id" title="var">_</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="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.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypePack"><span class="id" title="constructor">QuotTypePack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><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> <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><br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.invT"><span class="id" title="variable">invT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ssralg.html#GRing.inv"><span class="id" title="definition">GRing.inv</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.UnitRing.Pack"><span class="id" title="constructor">GRing.UnitRing.Pack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rc"><span class="id" title="variable">rc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.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><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Record</span> <a name="unit_ring_quot_class_of"><span class="id" title="record">unit_ring_quot_class_of</span></a> (<span class="id" title="var">Q</span> : <span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> := <a name="UnitRingQuotClass"><span class="id" title="constructor">UnitRingQuotClass</span></a> {<br/> + <a name="unit_ring_quot_quot_class"><span class="id" title="projection">unit_ring_quot_quot_class</span></a> :> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_class_of"><span class="id" title="abbreviation">quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>;<br/> + <a name="unit_ring_quot_ring_class"><span class="id" title="projection">unit_ring_quot_ring_class</span></a> :> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.UnitRing.class_of"><span class="id" title="record">GRing.UnitRing.class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>;<br/> + <a name="unit_ring_quot_mixin"><span class="id" title="projection">unit_ring_quot_mixin</span></a> :> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_mixin_of"><span class="id" title="record">unit_ring_quot_mixin_of</span></a><br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_quot_class"><span class="id" title="method">unit_ring_quot_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_ring_class"><span class="id" title="method">unit_ring_quot_ring_class</span></a><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Structure</span> <a name="unitRingQuotType"><span class="id" title="record">unitRingQuotType</span></a> : <span class="id" title="keyword">Type</span> := <a name="UnitRingQuotTypePack"><span class="id" title="constructor">UnitRingQuotTypePack</span></a> {<br/> + <a name="unit_ring_quot_sort"><span class="id" title="projection">unit_ring_quot_sort</span></a> :> <span class="id" title="keyword">Type</span>;<br/> + <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class_of"><span class="id" title="record">unit_ring_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_sort"><span class="id" title="method">unit_ring_quot_sort</span></a>;<br/> + <span class="id" title="var">_</span> : <span class="id" title="keyword">Type</span><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">rqT</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType"><span class="id" title="record">unitRingQuotType</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="unit_ring_quot_class"><span class="id" title="definition">unit_ring_quot_class</span></a> <span class="id" title="var">rqT</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class_of"><span class="id" title="record">unit_ring_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a> :=<br/> + <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuotTypePack"><span class="id" title="constructor">UnitRingQuotTypePack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">cT</span> <span class="id" title="var">_</span> <span class="id" title="keyword">as</span> <span class="id" title="var">qT'</span> := <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a><br/> + <span class="id" title="keyword">return</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class_of"><span class="id" title="record">unit_ring_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qT'"><span class="id" title="variable">qT'</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">cT</span>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="unit_ring_ring_quot_class"><span class="id" title="definition">unit_ring_ring_quot_class</span></a> <span class="id" title="var">rqT</span> (<span class="id" title="var">rqc</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class_of"><span class="id" title="record">unit_ring_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) :<br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class_of"><span class="id" title="record">ring_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.eqT"><span class="id" title="variable">eqT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.zeroT"><span class="id" title="variable">zeroT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.oppT"><span class="id" title="variable">oppT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.addT"><span class="id" title="variable">addT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.oneT"><span class="id" title="variable">oneT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.mulT"><span class="id" title="variable">mulT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a> := <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuotClass"><span class="id" title="constructor">RingQuotClass</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqc"><span class="id" title="variable">rqc</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="unit_ring_zmod_quot_class"><span class="id" title="definition">unit_ring_zmod_quot_class</span></a> <span class="id" title="var">rqT</span> (<span class="id" title="var">rqc</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class_of"><span class="id" title="record">unit_ring_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) :<br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class_of"><span class="id" title="record">zmod_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.eqT"><span class="id" title="variable">eqT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.zeroT"><span class="id" title="variable">zeroT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.oppT"><span class="id" title="variable">oppT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.addT"><span class="id" title="variable">addT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a> := <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuotClass"><span class="id" title="constructor">ZmodQuotClass</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqc"><span class="id" title="variable">rqc</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="unit_ring_eq_quot_class"><span class="id" title="definition">unit_ring_eq_quot_class</span></a> <span class="id" title="var">rqT</span> (<span class="id" title="var">rqc</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class_of"><span class="id" title="record">unit_ring_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) :<br/> + <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_class_of"><span class="id" title="record">eq_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.eqT"><span class="id" title="variable">eqT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotClass"><span class="id" title="constructor">EqQuotClass</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqc"><span class="id" title="variable">rqc</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">unitRingQuotType_eqType</span> <span class="id" title="var">rqT</span> :=<br/> + <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Pack"><span class="id" title="constructor">Equality.Pack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class"><span class="id" title="definition">unit_ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">unitRingQuotType_choiceType</span> <span class="id" title="var">rqT</span> :=<br/> + <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Pack"><span class="id" title="constructor">Choice.Pack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class"><span class="id" title="definition">unit_ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">unitRingQuotType_zmodType</span> <span class="id" title="var">rqT</span> :=<br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Pack"><span class="id" title="constructor">GRing.Zmodule.Pack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class"><span class="id" title="definition">unit_ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">unitRingQuotType_ringType</span> <span class="id" title="var">rqT</span> :=<br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Pack"><span class="id" title="constructor">GRing.Ring.Pack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class"><span class="id" title="definition">unit_ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">unitRingQuotType_unitRingType</span> <span class="id" title="var">rqT</span> :=<br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.UnitRing.Pack"><span class="id" title="constructor">GRing.UnitRing.Pack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class"><span class="id" title="definition">unit_ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">unitRingQuotType_quotType</span> <span class="id" title="var">rqT</span> :=<br/> + <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypePack"><span class="id" title="constructor">QuotTypePack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class"><span class="id" title="definition">unit_ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">unitRingQuotType_eqQuotType</span> <span class="id" title="var">rqT</span> :=<br/> + <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTypePack"><span class="id" title="constructor">EqQuotTypePack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_eq_quot_class"><span class="id" title="definition">unit_ring_eq_quot_class</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class"><span class="id" title="definition">unit_ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>)) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">unitRingQuotType_zmodQuotType</span> <span class="id" title="var">rqT</span> :=<br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuotTypePack"><span class="id" title="constructor">ZmodQuotTypePack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_zmod_quot_class"><span class="id" title="definition">unit_ring_zmod_quot_class</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class"><span class="id" title="definition">unit_ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>)) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">unitRingQuotType_ringQuotType</span> <span class="id" title="var">rqT</span> :=<br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuotTypePack"><span class="id" title="constructor">RingQuotTypePack</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_ring_quot_class"><span class="id" title="definition">unit_ring_ring_quot_class</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class"><span class="id" title="definition">unit_ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>)) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_eqType"><span class="id" title="definition">unitRingQuotType_eqType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_eqType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_eqType"><span class="id" title="definition">unitRingQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_eqType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_eqType"><span class="id" title="definition">eqType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_choiceType"><span class="id" title="definition">unitRingQuotType_choiceType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_choiceType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_choiceType"><span class="id" title="definition">unitRingQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_choiceType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_choiceType"><span class="id" title="definition">choiceType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_zmodType"><span class="id" title="definition">unitRingQuotType_zmodType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_zmodType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_zmodType"><span class="id" title="definition">unitRingQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_zmodType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_zmodType"><span class="id" title="definition">zmodType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_ringType"><span class="id" title="definition">unitRingQuotType_ringType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_ringType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_ringType"><span class="id" title="definition">unitRingQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_ringType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_ringType"><span class="id" title="definition">ringType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_unitRingType"><span class="id" title="definition">unitRingQuotType_unitRingType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_unitRingType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_unitRingType"><span class="id" title="definition">unitRingQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_unitRingType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_unitRingType"><span class="id" title="definition">unitRingType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_quotType"><span class="id" title="definition">unitRingQuotType_quotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_quotType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_quotType"><span class="id" title="definition">unitRingQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_quotType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_quotType"><span class="id" title="definition">quotType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_eqQuotType"><span class="id" title="definition">unitRingQuotType_eqQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_eqQuotType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_eqQuotType"><span class="id" title="definition">unitRingQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_eqQuotType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_eqQuotType"><span class="id" title="definition">eqQuotType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_zmodQuotType"><span class="id" title="definition">unitRingQuotType_zmodQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_zmodQuotType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_zmodQuotType"><span class="id" title="definition">unitRingQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_zmodQuotType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_zmodQuotType"><span class="id" title="definition">zmodQuotType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_ringQuotType"><span class="id" title="definition">unitRingQuotType_ringQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_ringQuotType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_ringQuotType"><span class="id" title="definition">unitRingQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_ringQuotType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#unitRingQuotType_ringQuotType"><span class="id" title="definition">ringQuotType</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="UnitRingQuotType_pack"><span class="id" title="definition">UnitRingQuotType_pack</span></a> <span class="id" title="var">Q</span> :=<br/> + <span class="id" title="keyword">fun</span> (<span class="id" title="var">qT</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.T"><span class="id" title="variable">T</span></a>) (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.UnitRing.Exports.unitRingType"><span class="id" title="abbreviation">unitRingType</span></a>) <span class="id" title="var">qc</span> <span class="id" title="var">rc</span><br/> + <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_class"><span class="id" title="projection">quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qT"><span class="id" title="variable">qT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> & <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.UnitRing.class"><span class="id" title="definition">GRing.UnitRing.class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rT"><span class="id" title="variable">rT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rc"><span class="id" title="variable">rc</span></a> ⇒<br/> + <span class="id" title="keyword">fun</span> <span class="id" title="var">m</span> ⇒ <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuotTypePack"><span class="id" title="constructor">UnitRingQuotTypePack</span></a> (@<a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuotClass"><span class="id" title="constructor">UnitRingQuotClass</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rc"><span class="id" title="variable">rc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#m"><span class="id" title="variable">m</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="UnitRingQuotMixin_pack"><span class="id" title="definition">UnitRingQuotMixin_pack</span></a> <span class="id" title="var">Q</span> :=<br/> + <span class="id" title="keyword">fun</span> (<span class="id" title="var">qT</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#ringQuotType"><span class="id" title="record">ringQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.eqT"><span class="id" title="variable">eqT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.zeroT"><span class="id" title="variable">zeroT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.oppT"><span class="id" title="variable">oppT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.addT"><span class="id" title="variable">addT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.oneT"><span class="id" title="variable">oneT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.mulT"><span class="id" title="variable">mulT</span></a>) ⇒<br/> + <span class="id" title="keyword">fun</span> (<span class="id" title="var">qc</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#ring_quot_class_of"><span class="id" title="record">ring_quot_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.eqT"><span class="id" title="variable">eqT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.zeroT"><span class="id" title="variable">zeroT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.oppT"><span class="id" title="variable">oppT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.addT"><span class="id" title="variable">addT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.oneT"><span class="id" title="variable">oneT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.mulT"><span class="id" title="variable">mulT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>)<br/> + <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_class"><span class="id" title="definition">zmod_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qT"><span class="id" title="variable">qT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> ⇒<br/> + <span class="id" title="keyword">fun</span> (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.UnitRing.Exports.unitRingType"><span class="id" title="abbreviation">unitRingType</span></a>) <span class="id" title="var">rc</span> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.UnitRing.class"><span class="id" title="definition">GRing.UnitRing.class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rT"><span class="id" title="variable">rT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#rc"><span class="id" title="variable">rc</span></a> ⇒<br/> + <span class="id" title="keyword">fun</span> <span class="id" title="var">mR</span> <span class="id" title="var">mU</span> <span class="id" title="var">mV</span> ⇒ @<a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuotMixinPack"><span class="id" title="constructor">UnitRingQuotMixinPack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rc"><span class="id" title="variable">rc</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#mR"><span class="id" title="variable">mR</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#mU"><span class="id" title="variable">mU</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#mV"><span class="id" title="variable">mV</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="UnitRingQuotType_clone"><span class="id" title="definition">UnitRingQuotType_clone</span></a> (<span class="id" title="var">Q</span> : <span class="id" title="keyword">Type</span>) <span class="id" title="var">qT</span> <span class="id" title="var">cT</span><br/> + <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class"><span class="id" title="definition">unit_ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#qT"><span class="id" title="variable">qT</span></a>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#cT"><span class="id" title="variable">cT</span></a> := @<a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuotTypePack"><span class="id" title="constructor">UnitRingQuotTypePack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#cT"><span class="id" title="variable">cT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Q"><span class="id" title="variable">Q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="unit_ring_quot_mixinP"><span class="id" title="lemma">unit_ring_quot_mixinP</span></a> <span class="id" title="var">rqT</span> :<br/> + <a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_mixin_of"><span class="id" title="record">unit_ring_quot_mixin_of</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class"><span class="id" title="definition">unit_ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>) (<a class="idref" href="mathcomp.algebra.ring_quotient.html#unit_ring_quot_class"><span class="id" title="definition">unit_ring_quot_class</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pi_unitr"><span class="id" title="lemma">pi_unitr</span></a> <span class="id" title="var">rqT</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fcecf6c7c5b99f975a4e95451ce580e5"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fcecf6c7c5b99f975a4e95451ce580e5"><span class="id" title="notation">mono</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_rqT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fcecf6c7c5b99f975a4e95451ce580e5"><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#fcecf6c7c5b99f975a4e95451ce580e5"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot.unitT"><span class="id" title="variable">unitT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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#fcecf6c7c5b99f975a4e95451ce580e5"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ssralg.html#GRing.unit"><span class="id" title="definition">GRing.unit</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fcecf6c7c5b99f975a4e95451ce580e5"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pi_invr"><span class="id" title="lemma">pi_invr</span></a> <span class="id" title="var">rqT</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="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.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_rqT</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.algebra.ring_quotient.html#UnitRingQuot.invT"><span class="id" title="variable">invT</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ring_quotient.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#f3016d4e55aa553d3e912592ec65e342"><span class="id" title="notation">^-1</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>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_unit_quot_morph</span> <span class="id" title="var">rqT</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiMono1"><span class="id" title="abbreviation">PiMono1</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#pi_unitr"><span class="id" title="lemma">pi_unitr</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>).<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_inv_quot_morph</span> <span class="id" title="var">rqT</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiMorph1"><span class="id" title="abbreviation">PiMorph1</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#pi_invr"><span class="id" title="lemma">pi_invr</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#rqT"><span class="id" title="variable">rqT</span></a>).<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuot"><span class="id" title="section">UnitRingQuot</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="UnitRingQuotType"><span class="id" title="abbreviation">UnitRingQuotType</span></a> <span class="id" title="var">u</span> <span class="id" title="var">i</span> <span class="id" title="var">Q</span> <span class="id" title="var">mix</span> :=<br/> + (@<a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuotType_pack"><span class="id" title="definition">UnitRingQuotType_pack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">u</span> <span class="id" title="var">i</span> <span class="id" title="var">Q</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">mix</span>).<br/> +<span class="id" title="keyword">Notation</span> <a name="1b5f59afaa9b0fca65e0abdceed3449f"><span class="id" title="notation">"</span></a>[ 'unitRingQuotType' u & i 'of' Q ]" :=<br/> + (@<a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuotType_clone"><span class="id" title="definition">UnitRingQuotType_clone</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">u</span> <span class="id" title="var">i</span> <span class="id" title="var">Q</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'unitRingQuotType' u & i 'of' Q ]") : <span class="id" title="var">form_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="UnitRingQuotMixin"><span class="id" title="abbreviation">UnitRingQuotMixin</span></a> <span class="id" title="var">Q</span> <span class="id" title="var">mU</span> <span class="id" title="var">mV</span> :=<br/> + (@<a class="idref" href="mathcomp.algebra.ring_quotient.html#UnitRingQuotMixin_pack"><span class="id" title="definition">UnitRingQuotMixin_pack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">Q</span><br/> + <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> (<a class="idref" href="mathcomp.algebra.ring_quotient.html#zmod_quot_mixinP"><span class="id" title="lemma">zmod_quot_mixinP</span></a> <span class="id" title="var">_</span>) <span class="id" title="var">mU</span> <span class="id" title="var">mV</span>).<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="IdealDef"><span class="id" title="section">IdealDef</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="proper_ideal"><span class="id" title="definition">proper_ideal</span></a> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</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#predPredType"><span class="id" title="definition">predPredType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#R"><span class="id" title="variable">R</span></a>) : <span class="id" title="keyword">Prop</span> :=<br/> + 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ad6d23746eb1a3b62e52010d3945a1db"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ad6d23746eb1a3b62e52010d3945a1db"><span class="id" title="notation">notin</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <span class="id" title="keyword">∀</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.algebra.ring_quotient.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#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">u</span>, <a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ring_quotient.html#u"><span class="id" title="variable">u</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.ring_quotient.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#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="prime_idealr_closed"><span class="id" title="definition">prime_idealr_closed</span></a> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</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#predPredType"><span class="id" title="definition">predPredType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#R"><span class="id" title="variable">R</span></a>) : <span class="id" title="keyword">Prop</span> :=<br/> + <span class="id" title="keyword">∀</span> <span class="id" title="var">u</span> <span class="id" title="var">v</span>, <a class="idref" href="mathcomp.algebra.ring_quotient.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#v"><span class="id" title="variable">v</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.ring_quotient.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.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ring_quotient.html#u"><span class="id" title="variable">u</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.ring_quotient.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.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">||</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ring_quotient.html#v"><span class="id" title="variable">v</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.ring_quotient.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.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="idealr_closed"><span class="id" title="definition">idealr_closed</span></a> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</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#predPredType"><span class="id" title="definition">predPredType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#R"><span class="id" title="variable">R</span></a>) :=<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">[/\</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.algebra.ring_quotient.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#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">,</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ad6d23746eb1a3b62e52010d3945a1db"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ad6d23746eb1a3b62e52010d3945a1db"><span class="id" title="notation">notin</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">&</span></a> <span class="id" title="keyword">∀</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#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.algebra.ring_quotient.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#2bba53854f326a714d377124cccec593"><span class="id" title="notation">&,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">u</span> <span class="id" title="var">v</span>, <a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ring_quotient.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#v"><span class="id" title="variable">v</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.ring_quotient.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#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#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="idealr_closed_nontrivial"><span class="id" title="lemma">idealr_closed_nontrivial</span></a> <span class="id" title="var">R</span> <span class="id" title="var">S</span> : @<a class="idref" href="mathcomp.algebra.ring_quotient.html#idealr_closed"><span class="id" title="definition">idealr_closed</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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="mathcomp.algebra.ring_quotient.html#proper_ideal"><span class="id" title="definition">proper_ideal</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#S"><span class="id" title="variable">S</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="idealr_closedB"><span class="id" title="lemma">idealr_closedB</span></a> <span class="id" title="var">R</span> <span class="id" title="var">S</span> : @<a class="idref" href="mathcomp.algebra.ring_quotient.html#idealr_closed"><span class="id" title="definition">idealr_closed</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.zmod_closed"><span class="id" title="abbreviation">zmod_closed</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#S"><span class="id" title="variable">S</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#idealr_closedB"><span class="id" title="lemma">idealr_closedB</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#idealr_closedB"><span class="id" title="lemma">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#idealr_closedB"><span class="id" title="lemma">idealr_closed</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#idealr_closedB"><span class="id" title="lemma">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#idealr_closedB"><span class="id" title="lemma">zmod_closed</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#idealr_closed_nontrivial"><span class="id" title="lemma">idealr_closed_nontrivial</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#idealr_closed_nontrivial"><span class="id" title="lemma">:</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#idealr_closed_nontrivial"><span class="id" title="lemma">idealr_closed</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#idealr_closed_nontrivial"><span class="id" title="lemma">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#idealr_closed_nontrivial"><span class="id" title="lemma">proper_ideal</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Structure</span> <a name="idealr"><span class="id" title="record">idealr</span></a> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</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#predPredType"><span class="id" title="definition">predPredType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#R"><span class="id" title="variable">R</span></a>) := <a name="MkIdeal"><span class="id" title="constructor">MkIdeal</span></a> {<br/> + <a name="idealr_zmod"><span class="id" title="projection">idealr_zmod</span></a> :> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.zmodPred"><span class="id" title="abbreviation">zmodPred</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#S"><span class="id" title="variable">S</span></a>;<br/> + <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#proper_ideal"><span class="id" title="definition">proper_ideal</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#S"><span class="id" title="variable">S</span></a><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Structure</span> <a name="prime_idealr"><span class="id" title="record">prime_idealr</span></a> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</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#predPredType"><span class="id" title="definition">predPredType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#R"><span class="id" title="variable">R</span></a>) := <a name="MkPrimeIdeal"><span class="id" title="constructor">MkPrimeIdeal</span></a> {<br/> + <a name="prime_idealr_zmod"><span class="id" title="projection">prime_idealr_zmod</span></a> :> <a class="idref" href="mathcomp.algebra.ring_quotient.html#idealr"><span class="id" title="record">idealr</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#S"><span class="id" title="variable">S</span></a>;<br/> + <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#prime_idealr_closed"><span class="id" title="definition">prime_idealr_closed</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#S"><span class="id" title="variable">S</span></a><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="Idealr"><span class="id" title="definition">Idealr</span></a> (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</span></a>) (<span class="id" title="var">I</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predPredType"><span class="id" title="definition">predPredType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#R"><span class="id" title="variable">R</span></a>) (<span class="id" title="var">zmodI</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.zmodPred"><span class="id" title="abbreviation">zmodPred</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#I"><span class="id" title="variable">I</span></a>)<br/> + (<span class="id" title="var">kI</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#keyed_pred"><span class="id" title="record">keyed_pred</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodI"><span class="id" title="variable">zmodI</span></a>) : <a class="idref" href="mathcomp.algebra.ring_quotient.html#proper_ideal"><span class="id" title="definition">proper_ideal</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#I"><span class="id" title="variable">I</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#idealr"><span class="id" title="record">idealr</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#I"><span class="id" title="variable">I</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="IdealDef.IdealTheory"><span class="id" title="section">IdealTheory</span></a>.<br/> +<span class="id" title="keyword">Variables</span> (<a name="IdealDef.IdealTheory.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</span></a>) (<a name="IdealDef.IdealTheory.I"><span class="id" title="variable">I</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predPredType"><span class="id" title="definition">predPredType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#R"><span class="id" title="variable">R</span></a>)<br/> + (<a name="IdealDef.IdealTheory.idealrI"><span class="id" title="variable">idealrI</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#idealr"><span class="id" title="record">idealr</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#I"><span class="id" title="variable">I</span></a>) (<a name="IdealDef.IdealTheory.kI"><span class="id" title="variable">kI</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#keyed_pred"><span class="id" title="record">keyed_pred</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#idealrI"><span class="id" title="variable">idealrI</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="idealr1"><span class="id" title="lemma">idealr1</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.algebra.ring_quotient.html#IdealDef.IdealTheory.kI"><span class="id" title="variable">kI</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.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="idealMr"><span class="id" title="lemma">idealMr</span></a> <span class="id" title="var">a</span> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#u"><span class="id" title="variable">u</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.ring_quotient.html#IdealDef.IdealTheory.kI"><span class="id" title="variable">kI</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ring_quotient.html#u"><span class="id" title="variable">u</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.ring_quotient.html#IdealDef.IdealTheory.kI"><span class="id" title="variable">kI</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="idealr0"><span class="id" title="lemma">idealr0</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.algebra.ring_quotient.html#IdealDef.IdealTheory.kI"><span class="id" title="variable">kI</span></a>. <br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#IdealDef.IdealTheory"><span class="id" title="section">IdealTheory</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="IdealDef.PrimeIdealTheory"><span class="id" title="section">PrimeIdealTheory</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="IdealDef.PrimeIdealTheory.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ComRing.Exports.comRingType"><span class="id" title="abbreviation">comRingType</span></a>) (<a name="IdealDef.PrimeIdealTheory.I"><span class="id" title="variable">I</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predPredType"><span class="id" title="definition">predPredType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#R"><span class="id" title="variable">R</span></a>)<br/> + (<a name="IdealDef.PrimeIdealTheory.pidealrI"><span class="id" title="variable">pidealrI</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#prime_idealr"><span class="id" title="record">prime_idealr</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#I"><span class="id" title="variable">I</span></a>) (<a name="IdealDef.PrimeIdealTheory.kI"><span class="id" title="variable">kI</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#keyed_pred"><span class="id" title="record">keyed_pred</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#pidealrI"><span class="id" title="variable">pidealrI</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="prime_idealrM"><span class="id" title="lemma">prime_idealrM</span></a> <span class="id" title="var">u</span> <span class="id" title="var">v</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.ring_quotient.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#v"><span class="id" title="variable">v</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.ring_quotient.html#IdealDef.PrimeIdealTheory.kI"><span class="id" title="variable">kI</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.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ring_quotient.html#u"><span class="id" title="variable">u</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.ring_quotient.html#IdealDef.PrimeIdealTheory.kI"><span class="id" title="variable">kI</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">||</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ring_quotient.html#v"><span class="id" title="variable">v</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.ring_quotient.html#IdealDef.PrimeIdealTheory.kI"><span class="id" title="variable">kI</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#IdealDef.PrimeIdealTheory"><span class="id" title="section">PrimeIdealTheory</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#IdealDef"><span class="id" title="section">IdealDef</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Module</span> <a name="Quotient"><span class="id" title="module">Quotient</span></a>.<br/> +<span class="id" title="keyword">Section</span> <a name="Quotient.ZmodQuotient"><span class="id" title="section">ZmodQuotient</span></a>.<br/> +<span class="id" title="keyword">Variables</span> (<a name="Quotient.ZmodQuotient.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Exports.zmodType"><span class="id" title="abbreviation">zmodType</span></a>) (<a name="Quotient.ZmodQuotient.I"><span class="id" title="variable">I</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predPredType"><span class="id" title="definition">predPredType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#R"><span class="id" title="variable">R</span></a>)<br/> + (<a name="Quotient.ZmodQuotient.zmodI"><span class="id" title="variable">zmodI</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Pred.Exports.zmodPred"><span class="id" title="abbreviation">zmodPred</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#I"><span class="id" title="variable">I</span></a>) (<a name="Quotient.ZmodQuotient.kI"><span class="id" title="variable">kI</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#keyed_pred"><span class="id" title="record">keyed_pred</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#zmodI"><span class="id" title="variable">zmodI</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="Quotient.equiv"><span class="id" title="definition">equiv</span></a> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.ZmodQuotient.R"><span class="id" title="variable">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="mathcomp.algebra.ring_quotient.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.algebra.ring_quotient.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#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">\</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.ring_quotient.html#Quotient.ZmodQuotient.kI"><span class="id" title="variable">kI</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Quotient.equivE"><span class="id" title="lemma">equivE</span></a> <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.algebra.ring_quotient.html#Quotient.equiv"><span class="id" title="definition">equiv</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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#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.algebra.ring_quotient.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.algebra.ring_quotient.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#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.ring_quotient.html#Quotient.ZmodQuotient.kI"><span class="id" title="variable">kI</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">Lemma</span> <a name="Quotient.equiv_is_equiv"><span class="id" title="lemma">equiv_is_equiv</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equiv_class_of"><span class="id" title="inductive">equiv_class_of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.equiv"><span class="id" title="definition">equiv</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">equiv_equiv</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRelPack"><span class="id" title="constructor">EquivRelPack</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.equiv_is_equiv"><span class="id" title="lemma">equiv_is_equiv</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">equiv_encModRel</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#defaultEncModRel"><span class="id" title="definition">defaultEncModRel</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.equiv"><span class="id" title="definition">equiv</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="Quotient.type"><span class="id" title="definition">type</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">eq_quot</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.equiv"><span class="id" title="definition">equiv</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="Quotient.type_of"><span class="id" title="definition">type_of</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.ZmodQuotient.R"><span class="id" title="variable">R</span></a> := <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="definition">type</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">rquot_quotType</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">rquot_eqType</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">rquot_choiceType</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">rquot_eqQuotType</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b7a0622a915c3e5a7396a3208b40639a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b7a0622a915c3e5a7396a3208b40639a"><span class="id" title="notation">eqQuotType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.equiv"><span class="id" title="definition">equiv</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b7a0622a915c3e5a7396a3208b40639a"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b7a0622a915c3e5a7396a3208b40639a"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Quotient.idealrBE"><span class="id" title="lemma">idealrBE</span></a> <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#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ring_quotient.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#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">\</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.ring_quotient.html#Quotient.ZmodQuotient.kI"><span class="id" title="variable">kI</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.ring_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><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>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Quotient.idealrDE"><span class="id" title="lemma">idealrDE</span></a> <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#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ring_quotient.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#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">\</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.ring_quotient.html#Quotient.ZmodQuotient.kI"><span class="id" title="variable">kI</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.ring_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><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.algebra.ring_quotient.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><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>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="Quotient.zero"><span class="id" title="definition">zero</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="definition">type</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#lift_cst"><span class="id" title="abbreviation">lift_cst</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="definition">type</span></a> 0.<br/> +<span class="id" title="keyword">Definition</span> <a name="Quotient.add"><span class="id" title="definition">add</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#lift_op2"><span class="id" title="abbreviation">lift_op2</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#327bb2f0da6fd7c01a004dedcfc2dee4"><span class="id" title="notation">+%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#327bb2f0da6fd7c01a004dedcfc2dee4"><span class="id" title="notation">R</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="Quotient.opp"><span class="id" title="definition">opp</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#lift_op1"><span class="id" title="abbreviation">lift_op1</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#9fdf1a446ceec36bc97cce801a3ef3f2"><span class="id" title="notation">-%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9fdf1a446ceec36bc97cce801a3ef3f2"><span class="id" title="notation">R</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_zero_morph</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiConst"><span class="id" title="abbreviation">PiConst</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.zero"><span class="id" title="definition">zero</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Quotient.pi_opp"><span class="id" title="lemma">pi_opp</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.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</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.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ring_quotient.html#Quotient.opp"><span class="id" title="definition">opp</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_opp_morph</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiMorph1"><span class="id" title="abbreviation">PiMorph1</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.pi_opp"><span class="id" title="lemma">pi_opp</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Quotient.pi_add"><span class="id" title="lemma">pi_add</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">:</span></a> <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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ring_quotient.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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.add"><span class="id" title="definition">add</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_add_morph</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiMorph2"><span class="id" title="abbreviation">PiMorph2</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.pi_add"><span class="id" title="lemma">pi_add</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Quotient.addqA"><span class="id" title="lemma">addqA</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#associative"><span class="id" title="definition">associative</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.add"><span class="id" title="definition">add</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Quotient.addqC"><span class="id" title="lemma">addqC</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#commutative"><span class="id" title="definition">commutative</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.add"><span class="id" title="definition">add</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Quotient.add0q"><span class="id" title="lemma">add0q</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#left_id"><span class="id" title="definition">left_id</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.zero"><span class="id" title="definition">zero</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.add"><span class="id" title="definition">add</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Quotient.addNq"><span class="id" title="lemma">addNq</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#left_inverse"><span class="id" title="definition">left_inverse</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.zero"><span class="id" title="definition">zero</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.opp"><span class="id" title="definition">opp</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.add"><span class="id" title="definition">add</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="Quotient.rquot_zmodMixin"><span class="id" title="definition">rquot_zmodMixin</span></a> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Exports.ZmodMixin"><span class="id" title="abbreviation">ZmodMixin</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.addqA"><span class="id" title="lemma">addqA</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.addqC"><span class="id" title="lemma">addqC</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.add0q"><span class="id" title="lemma">add0q</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.addNq"><span class="id" title="lemma">addNq</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">rquot_zmodType</span> := <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#GRing.Zmodule.Exports.ZmodType"><span class="id" title="abbreviation">ZmodType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.rquot_zmodMixin"><span class="id" title="definition">rquot_zmodMixin</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="Quotient.rquot_zmodQuotMixin"><span class="id" title="definition">rquot_zmodQuotMixin</span></a> := <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuotMixin"><span class="id" title="abbreviation">ZmodQuotMixin</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="definition">type</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#lock"><span class="id" title="lemma">lock</span></a> <span class="id" title="var">_</span>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.pi_opp"><span class="id" title="lemma">pi_opp</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.pi_add"><span class="id" title="lemma">pi_add</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">rquot_zmodQuotType</span> := <a class="idref" href="mathcomp.algebra.ring_quotient.html#ZmodQuotType"><span class="id" title="abbreviation">ZmodQuotType</span></a> 0 <a class="idref" href="mathcomp.algebra.ssralg.html#9fdf1a446ceec36bc97cce801a3ef3f2"><span class="id" title="notation">-%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9fdf1a446ceec36bc97cce801a3ef3f2"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#327bb2f0da6fd7c01a004dedcfc2dee4"><span class="id" title="notation">+%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#327bb2f0da6fd7c01a004dedcfc2dee4"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.rquot_zmodQuotMixin"><span class="id" title="definition">rquot_zmodQuotMixin</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.ZmodQuotient"><span class="id" title="section">ZmodQuotient</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="88169e749a9591eb9f0672e6db2adc1d"><span class="id" title="notation">"</span></a>{quot I }" := (@<a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type_of"><span class="id" title="definition">type_of</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">I</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">_</span>)).<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Quotient.RingQuotient"><span class="id" title="section">RingQuotient</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="Quotient.RingQuotient.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ComRing.Exports.comRingType"><span class="id" title="abbreviation">comRingType</span></a>) (<a name="Quotient.RingQuotient.I"><span class="id" title="variable">I</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predPredType"><span class="id" title="definition">predPredType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#R"><span class="id" title="variable">R</span></a>)<br/> + (<a name="Quotient.RingQuotient.idealI"><span class="id" title="variable">idealI</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#idealr"><span class="id" title="record">idealr</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#I"><span class="id" title="variable">I</span></a>) (<a name="Quotient.RingQuotient.kI"><span class="id" title="variable">kI</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#keyed_pred"><span class="id" title="record">keyed_pred</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#idealI"><span class="id" title="variable">idealI</span></a>).<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="Quotient.one"><span class="id" title="definition">one</span></a>: <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="abbreviation">type</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#lift_cst"><span class="id" title="abbreviation">lift_cst</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="abbreviation">type</span></a> 1.<br/> +<span class="id" title="keyword">Definition</span> <a name="Quotient.mul"><span class="id" title="definition">mul</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#lift_op2"><span class="id" title="abbreviation">lift_op2</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d5d4e2467843f67554f1a8a22d125de9"><span class="id" title="notation">*%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d5d4e2467843f67554f1a8a22d125de9"><span class="id" title="notation">R</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_one_morph</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiConst"><span class="id" title="abbreviation">PiConst</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.one"><span class="id" title="definition">one</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Quotient.pi_mul"><span class="id" title="lemma">pi_mul</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">:</span></a> <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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ring_quotient.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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.mul"><span class="id" title="definition">mul</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.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.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_mul_morph</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiMorph2"><span class="id" title="abbreviation">PiMorph2</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.pi_mul"><span class="id" title="lemma">pi_mul</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Quotient.mulqA"><span class="id" title="lemma">mulqA</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#associative"><span class="id" title="definition">associative</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.mul"><span class="id" title="definition">mul</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Quotient.mulqC"><span class="id" title="lemma">mulqC</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#commutative"><span class="id" title="definition">commutative</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.mul"><span class="id" title="definition">mul</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Quotient.mul1q"><span class="id" title="lemma">mul1q</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#left_id"><span class="id" title="definition">left_id</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.one"><span class="id" title="definition">one</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.mul"><span class="id" title="definition">mul</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Quotient.mulq_addl"><span class="id" title="lemma">mulq_addl</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#left_distributive"><span class="id" title="definition">left_distributive</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.mul"><span class="id" title="definition">mul</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#327bb2f0da6fd7c01a004dedcfc2dee4"><span class="id" title="notation">+%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#327bb2f0da6fd7c01a004dedcfc2dee4"><span class="id" title="notation">R</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Quotient.nonzero1q"><span class="id" title="lemma">nonzero1q</span></a>: <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.one"><span class="id" title="definition">one</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="Quotient.rquot_comRingMixin"><span class="id" title="definition">rquot_comRingMixin</span></a> :=<br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ComRing.Exports.ComRingMixin"><span class="id" title="abbreviation">ComRingMixin</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.mulqA"><span class="id" title="lemma">mulqA</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.mulqC"><span class="id" title="lemma">mulqC</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.mul1q"><span class="id" title="lemma">mul1q</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.mulq_addl"><span class="id" title="lemma">mulq_addl</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.nonzero1q"><span class="id" title="lemma">nonzero1q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">rquot_ringType</span> := <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#GRing.Ring.Exports.RingType"><span class="id" title="abbreviation">RingType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.rquot_comRingMixin"><span class="id" title="definition">rquot_comRingMixin</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">rquot_comRingType</span> := <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#GRing.ComRing.Exports.ComRingType"><span class="id" title="abbreviation">ComRingType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.mulqC"><span class="id" title="lemma">mulqC</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="Quotient.rquot_ringQuotMixin"><span class="id" title="definition">rquot_ringQuotMixin</span></a> := <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuotMixin"><span class="id" title="abbreviation">RingQuotMixin</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="abbreviation">type</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#lock"><span class="id" title="lemma">lock</span></a> <span class="id" title="var">_</span>) <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.pi_mul"><span class="id" title="lemma">pi_mul</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">rquot_ringQuotType</span> := <a class="idref" href="mathcomp.algebra.ring_quotient.html#RingQuotType"><span class="id" title="abbreviation">RingQuotType</span></a> 1 <a class="idref" href="mathcomp.algebra.ssralg.html#d5d4e2467843f67554f1a8a22d125de9"><span class="id" title="notation">*%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d5d4e2467843f67554f1a8a22d125de9"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.rquot_ringQuotMixin"><span class="id" title="definition">rquot_ringQuotMixin</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.RingQuotient"><span class="id" title="section">RingQuotient</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Quotient.IDomainQuotient"><span class="id" title="section">IDomainQuotient</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="Quotient.IDomainQuotient.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ComRing.Exports.comRingType"><span class="id" title="abbreviation">comRingType</span></a>) (<a name="Quotient.IDomainQuotient.I"><span class="id" title="variable">I</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predPredType"><span class="id" title="definition">predPredType</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#R"><span class="id" title="variable">R</span></a>)<br/> + (<a name="Quotient.IDomainQuotient.pidealI"><span class="id" title="variable">pidealI</span></a> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#prime_idealr"><span class="id" title="record">prime_idealr</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#I"><span class="id" title="variable">I</span></a>) (<a name="Quotient.IDomainQuotient.kI"><span class="id" title="variable">kI</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#keyed_pred"><span class="id" title="record">keyed_pred</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#pidealI"><span class="id" title="variable">pidealI</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Quotient.rquot_IdomainAxiom"><span class="id" title="lemma">rquot_IdomainAxiom</span></a> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.ring_quotient.html#88169e749a9591eb9f0672e6db2adc1d"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ring_quotient.html#88169e749a9591eb9f0672e6db2adc1d"><span class="id" title="notation">quot</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.IDomainQuotient.kI"><span class="id" title="variable">kI</span></a><a class="idref" href="mathcomp.algebra.ring_quotient.html#88169e749a9591eb9f0672e6db2adc1d"><span class="id" title="notation">}</span></a>): <a class="idref" href="mathcomp.algebra.ring_quotient.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.algebra.ring_quotient.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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ring_quotient.html#x"><span class="id" title="variable">x</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.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">||</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ring_quotient.html#y"><span class="id" title="variable">y</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.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient.IDomainQuotient"><span class="id" title="section">IDomainQuotient</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.ring_quotient.html#Quotient"><span class="id" title="module">Quotient</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="5eedbcbd3de3491e3e0645ec1f0ac7aa"><span class="id" title="notation">"</span></a>{ideal_quot I }" := (@<a class="idref" href="mathcomp.algebra.ring_quotient.html#type_of"><span class="id" title="definition">Quotient.type_of</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">I</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">_</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="196067f7d6bffa40cbf887ea96632cdc"><span class="id" title="notation">"</span></a>x == y %[mod_ideal I ]" :=<br/> + (<span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">==</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#5eedbcbd3de3491e3e0645ec1f0ac7aa"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ring_quotient.html#5eedbcbd3de3491e3e0645ec1f0ac7aa"><span class="id" title="notation">ideal_quot</span></a> <span class="id" title="var">I</span><a class="idref" href="mathcomp.algebra.ring_quotient.html#5eedbcbd3de3491e3e0645ec1f0ac7aa"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">]</span></a>) : <span class="id" title="var">quotient_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="c859a47d820a24af55974b4566666a01"><span class="id" title="notation">"</span></a>x = y %[mod_ideal I ]" :=<br/> + (<span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">=</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#5eedbcbd3de3491e3e0645ec1f0ac7aa"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ring_quotient.html#5eedbcbd3de3491e3e0645ec1f0ac7aa"><span class="id" title="notation">ideal_quot</span></a> <span class="id" title="var">I</span><a class="idref" href="mathcomp.algebra.ring_quotient.html#5eedbcbd3de3491e3e0645ec1f0ac7aa"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">]</span></a>) : <span class="id" title="var">quotient_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="cd4535596c25d791de7da2f2f60c5a5e"><span class="id" title="notation">"</span></a>x != y %[mod_ideal I ]" :=<br/> + (<span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#64dce3fc11e63c73e37431825b6bda70"><span class="id" title="notation">!=</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#64dce3fc11e63c73e37431825b6bda70"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#64dce3fc11e63c73e37431825b6bda70"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#5eedbcbd3de3491e3e0645ec1f0ac7aa"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ring_quotient.html#5eedbcbd3de3491e3e0645ec1f0ac7aa"><span class="id" title="notation">ideal_quot</span></a> <span class="id" title="var">I</span><a class="idref" href="mathcomp.algebra.ring_quotient.html#5eedbcbd3de3491e3e0645ec1f0ac7aa"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#64dce3fc11e63c73e37431825b6bda70"><span class="id" title="notation">]</span></a>) : <span class="id" title="var">quotient_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="879ec6e7c966bcda09371cc771e11f08"><span class="id" title="notation">"</span></a>x <> y %[mod_ideal I ]" :=<br/> + (<span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c19d82d8c4200cd8b2206f1641e1d5ca"><span class="id" title="notation">≠</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c19d82d8c4200cd8b2206f1641e1d5ca"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c19d82d8c4200cd8b2206f1641e1d5ca"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.algebra.ring_quotient.html#5eedbcbd3de3491e3e0645ec1f0ac7aa"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ring_quotient.html#5eedbcbd3de3491e3e0645ec1f0ac7aa"><span class="id" title="notation">ideal_quot</span></a> <span class="id" title="var">I</span><a class="idref" href="mathcomp.algebra.ring_quotient.html#5eedbcbd3de3491e3e0645ec1f0ac7aa"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c19d82d8c4200cd8b2206f1641e1d5ca"><span class="id" title="notation">]</span></a>) : <span class="id" title="var">quotient_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Quotient.rquot_eqType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Quotient.rquot_choiceType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Quotient.rquot_zmodType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Quotient.rquot_ringType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Quotient.rquot_comRingType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Quotient.rquot_quotType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Quotient.rquot_eqQuotType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Quotient.rquot_zmodQuotType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Quotient.rquot_ringQuotType</span>.<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 |