generate the documentation for 1.7

author: Enrico Tassi 2018-04-20 10:54:22 +0200
committer: Enrico Tassi 2018-04-20 10:54:22 +0200
commit: ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch)
tree: e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.algebra.fraction.html
parent: 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)
1 files changed, 434 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.algebra.fraction.html b/docs/htmldoc/mathcomp.algebra.fraction.html
new file mode 100644
index 0000000..2b78b50
--- /dev/null
+++ b/docs/htmldoc/mathcomp.algebra.fraction.html
@@ -0,0 +1,434 @@
+<!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.fraction</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library mathcomp.algebra.fraction</h1>
+
+<div class="code">
+<span class="comment">(*&nbsp;(c)&nbsp;Copyright&nbsp;2006-2016&nbsp;Microsoft&nbsp;Corporation&nbsp;and&nbsp;Inria.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
+&nbsp;Distributed&nbsp;under&nbsp;the&nbsp;terms&nbsp;of&nbsp;CeCILL-B.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ This file builds the field of fraction of any integral domain. 
+ The main result of this file is the existence of the field 
+ and of the tofrac function which is a injective ring morphism from R 
+ to its fraction field {fraction R}  
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Import</span> <span class="id" title="var">GRing.Theory</span>.<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> &quot;{ 'ratio' T }" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "{ 'ratio'  T }").<br/>
+<span class="id" title="keyword">Reserved Notation</span> &quot;{ 'fraction' T }" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "{ 'fraction'  T }").<br/>
+<span class="id" title="keyword">Reserved Notation</span> &quot;x %:F" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "x %:F").<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="FracDomain"><span class="id" title="section">FracDomain</span></a>.<br/>
+<span class="id" title="keyword">Variable</span> <a name="FracDomain.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>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ ratios are pairs of R, such that the second member is nonzero  
+</div>
+<div class="code">
+<span class="id" title="keyword">Inductive</span> <a name="ratio"><span class="id" title="record">ratio</span></a> := <a name="mkRatio"><span class="id" title="constructor">mkRatio</span></a> { <a name="frac"><span class="id" title="projection">frac</span></a> :&gt; <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.algebra.fraction.html#frac"><span class="id" title="method">frac</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 }.<br/>
+<span class="id" title="keyword">Definition</span> <a name="ratio_of"><span class="id" title="definition">ratio_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.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ratio_subType</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.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#frac"><span class="id" title="projection">frac</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ratio_of_subType</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.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="ratio_EqMixin"><span class="id" title="definition">ratio_EqMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ratio_eqType</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio_EqMixin"><span class="id" title="definition">ratio_EqMixin</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ratio_of_eqType</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.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.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="ratio_ChoiceMixin"><span class="id" title="definition">ratio_ChoiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ratio_choiceType</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio_ChoiceMixin"><span class="id" title="definition">ratio_ChoiceMixin</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ratio_of_choiceType</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.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.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="denom_ratioP"><span class="id" title="lemma">denom_ratioP</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a>, <a class="idref" href="mathcomp.algebra.fraction.html#f"><span class="id" title="variable">f</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</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="ratio0"><span class="id" title="definition">ratio0</span></a> := (@<a class="idref" href="mathcomp.algebra.fraction.html#mkRatio"><span class="id" title="constructor">mkRatio</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><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#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Theory.oner_neq0"><span class="id" title="definition">oner_neq0</span></a> <span class="id" title="var">_</span>)).<br/>
+<span class="id" title="keyword">Definition</span> <a name="Ratio"><span class="id" title="definition">Ratio</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">}</span></a> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#insubd"><span class="id" title="definition">insubd</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio0"><span class="id" title="definition">ratio0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.fraction.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.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="numer_Ratio"><span class="id" title="lemma">numer_Ratio</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.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#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">).1</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.fraction.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="denom_Ratio"><span class="id" title="lemma">denom_Ratio</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.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#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">).2</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.fraction.html#y"><span class="id" title="variable">y</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="numden_Ratio"><span class="id" title="definition">numden_Ratio</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#numer_Ratio"><span class="id" title="lemma">numer_Ratio</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#denom_Ratio"><span class="id" title="lemma">denom_Ratio</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">CoInductive</span> <a name="Ratio_spec"><span class="id" title="inductive">Ratio_spec</span></a> (<span class="id" title="var">n</span> <span class="id" title="var">d</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a>) : <a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Type</span> :=<br/>
+&nbsp;&nbsp;| <a name="RatioNull"><span class="id" title="constructor">RatioNull</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</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="mathcomp.algebra.fraction.html#Ratio_spec"><span class="id" title="inductive">Ratio_spec</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio0"><span class="id" title="definition">ratio0</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> 0<br/>
+&nbsp;&nbsp;| <a name="RatioNonNull"><span class="id" title="constructor">RatioNonNull</span></a> (<span class="id" title="var">d_neq0</span> : <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0) : <br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.fraction.html#Ratio_spec"><span class="id" title="inductive">Ratio_spec</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a> (@<a class="idref" href="mathcomp.algebra.fraction.html#mkRatio"><span class="id" title="constructor">mkRatio</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d_neq0"><span class="id" title="variable">d_neq0</span></a>) <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="RatioP"><span class="id" title="lemma">RatioP</span></a> <span class="id" title="var">n</span> <span class="id" title="var">d</span> : <a class="idref" href="mathcomp.algebra.fraction.html#Ratio_spec"><span class="id" title="inductive">Ratio_spec</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a> (<a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a>) <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="Ratio0"><span class="id" title="lemma">Ratio0</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio0"><span class="id" title="definition">ratio0</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain"><span class="id" title="section">FracDomain</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="d415e1de9145ec99991d83aeed2ffede"><span class="id" title="notation">&quot;</span></a>{ 'ratio' T }" := (<a class="idref" href="mathcomp.algebra.fraction.html#ratio_of"><span class="id" title="definition">ratio_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>)).<br/>
+<span class="id" title="keyword">Identity</span> <span class="id" title="keyword">Coercion</span> <span class="id" title="var">type_fracdomain_of</span> : <span class="id" title="var">ratio_of</span> &gt;-&gt; <span class="id" title="var">ratio</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">&quot;</span></a>'\n_' x"  := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#frac"><span class="id" title="projection">frac</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#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">).1</span></a><br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "'\n_' x").<br/>
+<span class="id" title="keyword">Notation</span> <a name="78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">&quot;</span></a>'\d_' x"  := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#frac"><span class="id" title="projection">frac</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#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">).2</span></a><br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "'\d_' x").<br/>
+
+<br/>
+<span class="id" title="keyword">Module</span> <a name="FracField"><span class="id" title="module">FracField</span></a>.<br/>
+<span class="id" title="keyword">Section</span> <a name="FracField.FracField"><span class="id" title="section">FracField</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="FracField.FracField.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.Exports.idomainType"><span class="id" title="abbreviation">idomainType</span></a>.<br/>
+
+<br/>
+
+<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.dom"><span class="id" title="abbreviation">dom</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ We define a relation in ratios  
+</div>
+<div class="code">
+<span class="id" title="keyword">Definition</span> <a name="FracField.equivf"><span class="id" title="definition">equivf</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> := <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf_notation"><span class="id" title="abbreviation">equivf_notation</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.equivfE"><span class="id" title="lemma">equivfE</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.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="mathcomp.algebra.fraction.html#FracField.equivf_notation"><span class="id" title="abbreviation">equivf_notation</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_refl"><span class="id" title="lemma">equivf_refl</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflexive"><span class="id" title="definition">reflexive</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_sym"><span class="id" title="lemma">equivf_sym</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#symmetric"><span class="id" title="definition">symmetric</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_trans"><span class="id" title="lemma">equivf_trans</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#transitive"><span class="id" title="definition">transitive</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ we show that equivf is an equivalence  
+</div>
+<div class="code">
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">equivf_equiv</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRel"><span class="id" title="abbreviation">EquivRel</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf_refl"><span class="id" title="lemma">equivf_refl</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf_sym"><span class="id" title="lemma">equivf_sym</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf_trans"><span class="id" title="lemma">equivf_trans</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="FracField.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.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</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="FracField.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.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">&quot;</span></a>{ 'fraction' T }" := (<a class="idref" href="mathcomp.algebra.fraction.html#FracField.type_of"><span class="id" title="definition">type_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>)).<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ we recover some structure for the quotient  
+</div>
+<div class="code">
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_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.fraction.html#FracField.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">frac_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.fraction.html#FracField.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">frac_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.fraction.html#FracField.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">frac_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.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</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.fraction.html#FracField.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">Canonical</span> <span class="id" title="var">frac_of_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.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</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">frac_of_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.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</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">frac_of_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.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</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">frac_of_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.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</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.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b7a0622a915c3e5a7396a3208b40639a"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ we explain what was the equivalence on the quotient  
+</div>
+<div class="code">
+<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_def"><span class="id" title="lemma">equivf_def</span></a> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a>) : <a class="idref" href="mathcomp.algebra.fraction.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.fraction.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.fraction.html#FracField.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><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_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.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_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.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_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>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_r"><span class="id" title="lemma">equivf_r</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_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.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</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_type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><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.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_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.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</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_type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">)</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_l"><span class="id" title="lemma">equivf_l</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</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_type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</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_type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.numer0"><span class="id" title="lemma">numer0</span></a> <span class="id" title="var">x</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.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_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.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.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec726891ee056b01e6c94482e2a4af00"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec726891ee056b01e6c94482e2a4af00"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#ratio0"><span class="id" title="definition">ratio0</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec726891ee056b01e6c94482e2a4af00"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec726891ee056b01e6c94482e2a4af00"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec726891ee056b01e6c94482e2a4af00"><span class="id" title="notation">mod_eq</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec726891ee056b01e6c94482e2a4af00"><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="FracField.Ratio_numden"><span class="id" title="lemma">Ratio_numden</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="FracField.tofrac"><span class="id" title="definition">tofrac</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#lift_embed"><span class="id" title="abbreviation">lift_embed</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a> ⇒ <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> 1).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tofrac_pi_morph</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiEmbed"><span class="id" title="abbreviation">PiEmbed</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.tofrac"><span class="id" title="definition">tofrac</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">&quot;</span></a>x %:F"  := (@<a class="idref" href="mathcomp.algebra.fraction.html#FracField.tofrac"><span class="id" title="definition">tofrac</span></a> <span class="id" title="var">x</span>).<br/>
+
+<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> <span class="id" title="var">c</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="FracField.addf"><span class="id" title="definition">addf</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.dom"><span class="id" title="abbreviation">dom</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> (<a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_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.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_y</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_y</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_x</span></a>) (<a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_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.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_y</span></a>).<br/>
+<span class="id" title="keyword">Definition</span> <a name="FracField.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.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.addf"><span class="id" title="definition">addf</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.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.fraction.html#FracField.addf"><span class="id" title="definition">addf</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.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">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add"><span class="id" title="definition">add</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.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.fraction.html#FracField.pi_add"><span class="id" title="lemma">pi_add</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="FracField.oppf"><span class="id" title="definition">oppf</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.dom"><span class="id" title="abbreviation">dom</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_x</span></a>) <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_x</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="FracField.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.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.oppf"><span class="id" title="definition">oppf</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.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.fraction.html#FracField.oppf"><span class="id" title="definition">oppf</span></a> <a class="idref" href="mathcomp.algebra.fraction.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">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.opp"><span class="id" title="definition">opp</span></a> <a class="idref" href="mathcomp.algebra.fraction.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="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.fraction.html#FracField.pi_opp"><span class="id" title="lemma">pi_opp</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="FracField.mulf"><span class="id" title="definition">mulf</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.dom"><span class="id" title="abbreviation">dom</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> (<a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_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.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_y</span></a>) (<a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_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.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_y</span></a>).<br/>
+<span class="id" title="keyword">Definition</span> <a name="FracField.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.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mulf"><span class="id" title="definition">mulf</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.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.fraction.html#FracField.mulf"><span class="id" title="definition">mulf</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.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">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.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.fraction.html#FracField.pi_mul"><span class="id" title="lemma">pi_mul</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="FracField.invf"><span class="id" title="definition">invf</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.dom"><span class="id" title="abbreviation">dom</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_x</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="FracField.inv"><span class="id" title="definition">inv</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.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.invf"><span class="id" title="definition">invf</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.pi_inv"><span class="id" title="lemma">pi_inv</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.fraction.html#FracField.invf"><span class="id" title="definition">invf</span></a> <a class="idref" href="mathcomp.algebra.fraction.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">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.inv"><span class="id" title="definition">inv</span></a> <a class="idref" href="mathcomp.algebra.fraction.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="keyword">Canonical</span> <span class="id" title="var">pi_inv_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.fraction.html#FracField.pi_inv"><span class="id" title="lemma">pi_inv</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.addA"><span class="id" title="lemma">addA</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.fraction.html#FracField.add"><span class="id" title="definition">add</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.addC"><span class="id" title="lemma">addC</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.fraction.html#FracField.add"><span class="id" title="definition">add</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.add0_l"><span class="id" title="lemma">add0_l</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> 0<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add"><span class="id" title="definition">add</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.addN_l"><span class="id" title="lemma">addN_l</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> 0<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.opp"><span class="id" title="definition">opp</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add"><span class="id" title="definition">add</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ fracions form an abelian group  
+</div>
+<div class="code">
+<span class="id" title="keyword">Definition</span> <a name="FracField.frac_zmodMixin"><span class="id" title="definition">frac_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.fraction.html#FracField.addA"><span class="id" title="lemma">addA</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.addC"><span class="id" title="lemma">addC</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add0_l"><span class="id" title="lemma">add0_l</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.addN_l"><span class="id" title="lemma">addN_l</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_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.fraction.html#FracField.type"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.frac_zmodMixin"><span class="id" title="definition">frac_zmodMixin</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.mulA"><span class="id" title="lemma">mulA</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.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.mulC"><span class="id" title="lemma">mulC</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.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.mul1_l"><span class="id" title="lemma">mul1_l</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#left_id"><span class="id" title="definition">left_id</span></a> 1<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.mul_addl"><span class="id" title="lemma">mul_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.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add"><span class="id" title="definition">add</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.nonzero1"><span class="id" title="lemma">nonzero1</span></a> : 1<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#9e45f909d1732d6d9e153b650829bccf"><span class="id" title="notation">!=</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#9e45f909d1732d6d9e153b650829bccf"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a>.<br/>
+ 
+<br/>
+</div>
+
+<div class="doc">
+ fracions form a commutative ring  
+</div>
+<div class="code">
+<span class="id" title="keyword">Definition</span> <a name="FracField.frac_comRingMixin"><span class="id" title="definition">frac_comRingMixin</span></a> := <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.fraction.html#FracField.mulA"><span class="id" title="lemma">mulA</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mulC"><span class="id" title="lemma">mulC</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mul1_l"><span class="id" title="lemma">mul1_l</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mul_addl"><span class="id" title="lemma">mul_addl</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.nonzero1"><span class="id" title="lemma">nonzero1</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_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.fraction.html#FracField.type"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.frac_comRingMixin"><span class="id" title="definition">frac_comRingMixin</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_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.fraction.html#FracField.type"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mulC"><span class="id" title="lemma">mulC</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.mulV_l"><span class="id" title="lemma">mulV_l</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">a</span>, <a class="idref" href="mathcomp.algebra.fraction.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</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.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a> (<a class="idref" href="mathcomp.algebra.fraction.html#FracField.inv"><span class="id" title="definition">inv</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#a"><span class="id" title="variable">a</span></a>) <a class="idref" href="mathcomp.algebra.fraction.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.inv0"><span class="id" title="lemma">inv0</span></a> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.inv"><span class="id" title="definition">inv</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</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="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ fractions form a ring with explicit unit  
+</div>
+<div class="code">
+<span class="id" title="keyword">Definition</span> <a name="FracField.RatFieldUnitMixin"><span class="id" title="definition">RatFieldUnitMixin</span></a> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.FieldUnitMixin"><span class="id" title="abbreviation">FieldUnitMixin</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mulV_l"><span class="id" title="lemma">mulV_l</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.inv0"><span class="id" title="lemma">inv0</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_unitRingType</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.UnitRing.Exports.UnitRingType"><span class="id" title="abbreviation">UnitRingType</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.RatFieldUnitMixin"><span class="id" title="definition">RatFieldUnitMixin</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_comUnitRingType</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">comUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FracField.field_axiom"><span class="id" title="lemma">field_axiom</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.mixin_of"><span class="id" title="definition">GRing.Field.mixin_of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.frac_unitRingType"><span class="id" title="definition">frac_unitRingType</span></a>.<br/>
+ 
+<br/>
+</div>
+
+<div class="doc">
+ fractions form a field  
+</div>
+<div class="code">
+<span class="id" title="keyword">Definition</span> <a name="FracField.RatFieldIdomainMixin"><span class="id" title="definition">RatFieldIdomainMixin</span></a> := (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.FieldIdomainMixin"><span class="id" title="abbreviation">FieldIdomainMixin</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.field_axiom"><span class="id" title="lemma">field_axiom</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_idomainType</span> :=<br/>
+&nbsp;&nbsp;<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.IntegralDomain.Exports.IdomainType"><span class="id" title="abbreviation">IdomainType</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.FieldIdomainMixin"><span class="id" title="abbreviation">FieldIdomainMixin</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.field_axiom"><span class="id" title="lemma">field_axiom</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_fieldType</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.FieldType"><span class="id" title="abbreviation">FieldType</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.field_axiom"><span class="id" title="lemma">field_axiom</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField"><span class="id" title="section">FracField</span></a>.<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.fraction.html#FracField"><span class="id" title="module">FracField</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">&quot;</span></a>{ 'fraction' T }" := (<a class="idref" href="mathcomp.algebra.fraction.html#type_of"><span class="id" title="definition">FracField.type_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>)).<br/>
+<span class="id" title="keyword">Notation</span> <a name="equivf"><span class="id" title="abbreviation">equivf</span></a> := (@<a class="idref" href="mathcomp.algebra.fraction.html#equivf"><span class="id" title="definition">FracField.equivf</span></a> <span class="id" title="var">_</span>).<br/>
+<span class="id" title="keyword">Hint Resolve</span> <span class="id" title="var">denom_ratioP</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="Canonicals"><span class="id" title="section">Canonicals</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="Canonicals.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.Exports.idomainType"><span class="id" title="abbreviation">idomainType</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ reexporting the structures  
+</div>
+<div class="code">
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FracField.frac_quotType</span>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FracField.frac_eqType</span>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FracField.frac_choiceType</span>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FracField.frac_zmodType</span>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FracField.frac_ringType</span>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FracField.frac_comRingType</span>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FracField.frac_unitRingType</span>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FracField.frac_comUnitRingType</span>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FracField.frac_idomainType</span>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FracField.frac_fieldType</span>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FracField.tofrac_pi_morph</span>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_quotType</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.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.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</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">frac_of_eqType</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.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.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</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">frac_of_choiceType</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.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.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</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">frac_of_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#af6385fc2df84aeeec6855073f75cc68"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af6385fc2df84aeeec6855073f75cc68"><span class="id" title="notation">zmodType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#af6385fc2df84aeeec6855073f75cc68"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af6385fc2df84aeeec6855073f75cc68"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_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#dee4f3431027813095272c568fc6b5ce"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#dee4f3431027813095272c568fc6b5ce"><span class="id" title="notation">ringType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#dee4f3431027813095272c568fc6b5ce"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#dee4f3431027813095272c568fc6b5ce"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_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#57b384122345a94c564987d4b6ee9f0f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#57b384122345a94c564987d4b6ee9f0f"><span class="id" title="notation">comRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#57b384122345a94c564987d4b6ee9f0f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#57b384122345a94c564987d4b6ee9f0f"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_unitRingType</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#f02859ca87d7563e473a6ba817bdc33f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#f02859ca87d7563e473a6ba817bdc33f"><span class="id" title="notation">unitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#f02859ca87d7563e473a6ba817bdc33f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#f02859ca87d7563e473a6ba817bdc33f"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_comUnitRingType</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#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">comUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_idomainType</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#9894f8fff6e44a40eb9fd9cfcbde7780"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9894f8fff6e44a40eb9fd9cfcbde7780"><span class="id" title="notation">idomainType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#9894f8fff6e44a40eb9fd9cfcbde7780"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9894f8fff6e44a40eb9fd9cfcbde7780"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_fieldType</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#005edfce3bb0bbe988e3333ca30adc0f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#005edfce3bb0bbe988e3333ca30adc0f"><span class="id" title="notation">fieldType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#005edfce3bb0bbe988e3333ca30adc0f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#005edfce3bb0bbe988e3333ca30adc0f"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals"><span class="id" title="section">Canonicals</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="FracFieldTheory"><span class="id" title="section">FracFieldTheory</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Import</span> <span class="id" title="var">FracField</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="FracFieldTheory.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.Exports.idomainType"><span class="id" title="abbreviation">idomainType</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="Ratio_numden"><span class="id" title="lemma">Ratio_numden</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#d415e1de9145ec99991d83aeed2ffede"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d415e1de9145ec99991d83aeed2ffede"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracFieldTheory.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d415e1de9145ec99991d83aeed2ffede"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+</div>
+
+<div class="doc">
+ exporting the embeding from R to {fraction R}  
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tofrac_is_additive"><span class="id" title="lemma">tofrac_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.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tofrac_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.fraction.html#tofrac_is_additive"><span class="id" title="lemma">tofrac_is_additive</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tofrac_is_multiplicative"><span class="id" title="lemma">tofrac_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.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tofrac_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.fraction.html#tofrac_is_multiplicative"><span class="id" title="lemma">tofrac_is_multiplicative</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ tests  
+</div>
+<div class="code">
+<span class="id" title="keyword">Lemma</span> <a name="tofrac0"><span class="id" title="lemma">tofrac0</span></a> : 0<a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">F</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/>
+<span class="id" title="keyword">Lemma</span> <a name="tofracN"><span class="id" title="lemma">tofracN</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><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#c3c88e2b30b681cd767a54649faf5973"><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.fraction.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#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">}</span></a>.  <br/>
+<span class="id" title="keyword">Lemma</span> <a name="tofracD"><span class="id" title="lemma">tofracD</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">:</span></a> <span class="id" title="var">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#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.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.fraction.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#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">}</span></a>.  <br/>
+<span class="id" title="keyword">Lemma</span> <a name="tofracB"><span class="id" title="lemma">tofracB</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">:</span></a> <span class="id" title="var">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#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.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.fraction.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#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">}</span></a>.  <br/>
+<span class="id" title="keyword">Lemma</span> <a name="tofracMn"><span class="id" title="lemma">tofracMn</span></a> <span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><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#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#891e51846c7d1d63a9cb5458374cf308"><span class="id" title="notation">*+</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">}</span></a>.  <br/>
+<span class="id" title="keyword">Lemma</span> <a name="tofracMNn"><span class="id" title="lemma">tofracMNn</span></a> <span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><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#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#3baee4193385688d2f1fcb170107cf5b"><span class="id" title="notation">*-</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">}</span></a>.  <br/>
+<span class="id" title="keyword">Lemma</span> <a name="tofrac1"><span class="id" title="lemma">tofrac1</span></a> : 1<a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">F</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/>
+<span class="id" title="keyword">Lemma</span> <a name="tofracM"><span class="id" title="lemma">tofracM</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">:</span></a> <span class="id" title="var">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#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.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.fraction.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#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">}</span></a>.  <br/>
+<span class="id" title="keyword">Lemma</span> <a name="tofracX"><span class="id" title="lemma">tofracX</span></a> <span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><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#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">}</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tofrac_eq"><span class="id" title="lemma">tofrac_eq</span></a> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracFieldTheory.R"><span class="id" title="variable">R</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.fraction.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">F</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.fraction.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#q"><span class="id" title="variable">q</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="tofrac_eq0"><span class="id" title="lemma">tofrac_eq0</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracFieldTheory.R"><span class="id" title="variable">R</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.fraction.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">F</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.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.fraction.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
+ <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.fraction.html#FracFieldTheory"><span class="id" title="section">FracFieldTheory</span></a>.<br/>
+</div>
+</div>
+
+<div id="footer">
+<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
+</div>
+
+</div>
+
+</body>
+</html>
+\ No newline at end of file
author	Enrico Tassi	2018-04-20 10:54:22 +0200
committer	Enrico Tassi	2018-04-20 10:54:22 +0200
commit	ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch)
tree	e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.algebra.fraction.html
parent	3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)