diff options
| author | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
| commit | 6b59540a2460633df4e3d8347cb4dfe2fb3a3afb (patch) | |
| tree | 1239c1d5553d51a7d73f2f8b465f6a23178ff8a0 /docs/htmldoc/mathcomp.algebra.fraction.html | |
| parent | dd82aaeae7e9478efc178ce8430986649555b032 (diff) | |
removing everything but index which redirects to the new page
Diffstat (limited to 'docs/htmldoc/mathcomp.algebra.fraction.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.algebra.fraction.html | 433 |
1 files changed, 0 insertions, 433 deletions
diff --git a/docs/htmldoc/mathcomp.algebra.fraction.html b/docs/htmldoc/mathcomp.algebra.fraction.html deleted file mode 100644 index 745fa06..0000000 --- a/docs/htmldoc/mathcomp.algebra.fraction.html +++ /dev/null @@ -1,433 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" -"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.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">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> - Distributed under the terms of CeCILL-B. *)</span><br/> - -<br/> -</div> - -<div class="doc"> - This file 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> "{ '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> "{ '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> "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> :> <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/V8.9.0/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><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/V8.9.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#c2d02b544d823cdc1e1e08de552cdba4"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#c2d02b544d823cdc1e1e08de552cdba4"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c2d02b544d823cdc1e1e08de552cdba4"><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#c2d02b544d823cdc1e1e08de552cdba4"><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#aa8c179e7d847b79500c7558a661edb0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#aa8c179e7d847b79500c7558a661edb0"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#aa8c179e7d847b79500c7558a661edb0"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><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#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#aa8c179e7d847b79500c7558a661edb0"><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#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><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#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation"><:]</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#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><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#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><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#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><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#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation"><:]</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#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><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#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><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/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><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#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><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#50c2e3815a42123311bc4308989023fc"><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/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><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/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><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/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><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#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">).1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.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#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">).2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.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/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><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/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><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/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variant</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#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><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#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Type</span> :=<br/> - | <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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/> - | <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#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0) : <br/> - <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/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><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/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><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/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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="03823952a2553ec6b46621aa2d9ce68e"><span class="id" title="notation">"</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/V8.9.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> >-> <span class="id" title="var">ratio</span>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">"</span></a>'\n_' x" := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">).1</span></a><br/> - (<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="e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">"</span></a>'\d_' x" := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">).2</span></a><br/> - (<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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.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/V8.9.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/V8.9.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#0dc587318a1236d89082bca629a5db9b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#0dc587318a1236d89082bca629a5db9b"><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#0dc587318a1236d89082bca629a5db9b"><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/V8.9.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="563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">"</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/V8.9.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#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><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#2b6ecaeff71b4103d20b05dbc196dba6"><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#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_choiceType</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_eqQuotType</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#dc3d569865bd181e003ea2b17400befd"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#dc3d569865bd181e003ea2b17400befd"><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#dc3d569865bd181e003ea2b17400befd"><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#dc3d569865bd181e003ea2b17400befd"><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#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><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#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><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#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><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#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_choiceType</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><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#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_eqQuotType</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#dc3d569865bd181e003ea2b17400befd"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#dc3d569865bd181e003ea2b17400befd"><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#dc3d569865bd181e003ea2b17400befd"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><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#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#dc3d569865bd181e003ea2b17400befd"><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#e3392789fbfaf247c0fb823980d6e8ff"><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#e3392789fbfaf247c0fb823980d6e8ff"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e3392789fbfaf247c0fb823980d6e8ff"><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#e3392789fbfaf247c0fb823980d6e8ff"><span class="id" title="notation">]</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">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#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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#14ffbcbb027e0dd70b8653f98ff33b0b"><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#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3799fc59ee103320fa3882288df6a9c4"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3799fc59ee103320fa3882288df6a9c4"><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#3799fc59ee103320fa3882288df6a9c4"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3799fc59ee103320fa3882288df6a9c4"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3799fc59ee103320fa3882288df6a9c4"><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#3799fc59ee103320fa3882288df6a9c4"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<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#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.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#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><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#563ad5e6433eb405cbb9f8f75f49cdce"><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="43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">"</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#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_y</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_y</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a>) (<a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><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#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><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#563ad5e6433eb405cbb9f8f75f49cdce"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">>-></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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><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#8d0566c961139ec21811f52ef0c317db"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a>) <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><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#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><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#563ad5e6433eb405cbb9f8f75f49cdce"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">>-></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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><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#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_y</span></a>) (<a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><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#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><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#563ad5e6433eb405cbb9f8f75f49cdce"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><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#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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><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#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><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#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><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#563ad5e6433eb405cbb9f8f75f49cdce"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">>-></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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><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/V8.9.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/V8.9.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/V8.9.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#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><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/V8.9.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#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><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/V8.9.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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#left_id"><span class="id" title="definition">left_id</span></a> 1<a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><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/V8.9.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#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#228e85e3c31a939cba019f255574c875"><span class="id" title="notation">!=</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#228e85e3c31a939cba019f255574c875"><span class="id" title="notation">:></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#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1<a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><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#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><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#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">comUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><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/> - <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="3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">"</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/V8.9.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> : <span class="id" title="var">core</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#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><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#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><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#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><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#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">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#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><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#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">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#97b11d2a158d9db11032c2626798c6ac"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#97b11d2a158d9db11032c2626798c6ac"><span class="id" title="notation">zmodType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#97b11d2a158d9db11032c2626798c6ac"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><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#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#97b11d2a158d9db11032c2626798c6ac"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">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#964cf6dee45a836ccf0bcd3d85de1071"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#964cf6dee45a836ccf0bcd3d85de1071"><span class="id" title="notation">ringType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#964cf6dee45a836ccf0bcd3d85de1071"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><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#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#964cf6dee45a836ccf0bcd3d85de1071"><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#8b92acac231ba6173223cf75164fca3d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#8b92acac231ba6173223cf75164fca3d"><span class="id" title="notation">comRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#8b92acac231ba6173223cf75164fca3d"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><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#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#8b92acac231ba6173223cf75164fca3d"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">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#2734494507570795a22f59746d1c0f0e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2734494507570795a22f59746d1c0f0e"><span class="id" title="notation">unitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2734494507570795a22f59746d1c0f0e"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><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#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2734494507570795a22f59746d1c0f0e"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">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#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">comUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><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#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">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#b10128495340407de3c7b321ce0c78de"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b10128495340407de3c7b321ce0c78de"><span class="id" title="notation">idomainType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#b10128495340407de3c7b321ce0c78de"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><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#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b10128495340407de3c7b321ce0c78de"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">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#be36f4c61e9a82f836d531a63f34e6c2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#be36f4c61e9a82f836d531a63f34e6c2"><span class="id" title="notation">fieldType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#be36f4c61e9a82f836d531a63f34e6c2"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><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#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#be36f4c61e9a82f836d531a63f34e6c2"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">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#03823952a2553ec6b46621aa2d9ce68e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#03823952a2553ec6b46621aa2d9ce68e"><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#03823952a2553ec6b46621aa2d9ce68e"><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#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.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#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#8d0566c961139ec21811f52ef0c317db"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#51dc792c356ca1a71a3094b50d6bb2fb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><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#e9001f602764f7896bb1eb34bf606a23"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><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#e4d9eba2da60fcfead1a1c78283587ed"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><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#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1. <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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><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#663140372ac3b275aae871b74b140513"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><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#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">F</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<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 |