diff options
| author | Enrico Tassi | 2019-05-22 13:43:08 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-05-22 15:34:14 +0200 |
| commit | 748d716efb2f2f75946c8386e441ce1789806a39 (patch) | |
| tree | fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/index_global_N.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/index_global_N.html')
| -rw-r--r-- | docs/htmldoc/index_global_N.html | 334 |
1 files changed, 213 insertions, 121 deletions
diff --git a/docs/htmldoc/index_global_N.html b/docs/htmldoc/index_global_N.html index 46ac872..38c24c8 100644 --- a/docs/htmldoc/index_global_N.html +++ b/docs/htmldoc/index_global_N.html @@ -4,7 +4,7 @@ <head> <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.ssreflect.tuple</title> +<title>mathcomp.test_suite.hierarchy_test</title> </head> <body> @@ -47,7 +47,7 @@ <td><a href="index_global_Z.html">Z</a></td> <td>_</td> <td><a href="index_global_*.html">other</a></td> -<td>(23233 entries)</td> +<td>(23836 entries)</td> </tr> <tr> <td>Notation Index</td> @@ -79,14 +79,14 @@ <td><a href="index_notation_Z.html">Z</a></td> <td>_</td> <td><a href="index_notation_*.html">other</a></td> -<td>(1373 entries)</td> +<td>(1409 entries)</td> </tr> <tr> <td>Module Index</td> <td><a href="index_module_A.html">A</a></td> <td><a href="index_module_B.html">B</a></td> <td><a href="index_module_C.html">C</a></td> -<td>D</td> +<td><a href="index_module_D.html">D</a></td> <td><a href="index_module_E.html">E</a></td> <td><a href="index_module_F.html">F</a></td> <td><a href="index_module_G.html">G</a></td> @@ -111,7 +111,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(213 entries)</td> +<td>(221 entries)</td> </tr> <tr> <td>Variable Index</td> @@ -143,7 +143,7 @@ <td><a href="index_variable_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(3475 entries)</td> +<td>(3574 entries)</td> </tr> <tr> <td>Library Index</td> @@ -175,7 +175,7 @@ <td><a href="index_library_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(89 entries)</td> +<td>(90 entries)</td> </tr> <tr> <td>Lemma Index</td> @@ -207,7 +207,7 @@ <td><a href="index_lemma_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(11853 entries)</td> +<td>(12096 entries)</td> </tr> <tr> <td>Constructor Index</td> @@ -239,7 +239,7 @@ <td><a href="index_constructor_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(359 entries)</td> +<td>(368 entries)</td> </tr> <tr> <td>Axiom Index</td> @@ -271,7 +271,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(47 entries)</td> +<td>(45 entries)</td> </tr> <tr> <td>Inductive Index</td> @@ -303,14 +303,14 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(103 entries)</td> +<td>(107 entries)</td> </tr> <tr> <td>Projection Index</td> <td><a href="index_projection_A.html">A</a></td> <td><a href="index_projection_B.html">B</a></td> <td><a href="index_projection_C.html">C</a></td> -<td>D</td> +<td><a href="index_projection_D.html">D</a></td> <td><a href="index_projection_E.html">E</a></td> <td><a href="index_projection_F.html">F</a></td> <td><a href="index_projection_G.html">G</a></td> @@ -335,7 +335,7 @@ <td><a href="index_projection_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(266 entries)</td> +<td>(273 entries)</td> </tr> <tr> <td>Section Index</td> @@ -367,7 +367,7 @@ <td><a href="index_section_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(1118 entries)</td> +<td>(1140 entries)</td> </tr> <tr> <td>Abbreviation Index</td> @@ -399,7 +399,7 @@ <td><a href="index_abbreviation_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(691 entries)</td> +<td>(728 entries)</td> </tr> <tr> <td>Definition Index</td> @@ -431,14 +431,14 @@ <td><a href="index_definition_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(3461 entries)</td> +<td>(3596 entries)</td> </tr> <tr> <td>Record Index</td> <td><a href="index_record_A.html">A</a></td> <td>B</td> <td><a href="index_record_C.html">C</a></td> -<td>D</td> +<td><a href="index_record_D.html">D</a></td> <td><a href="index_record_E.html">E</a></td> <td><a href="index_record_F.html">F</a></td> <td><a href="index_record_G.html">G</a></td> @@ -463,7 +463,7 @@ <td><a href="index_record_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(185 entries)</td> +<td>(189 entries)</td> </tr> </table> <hr/><a name="global_N"></a><h2>N </h2> @@ -490,7 +490,6 @@ <a href="mathcomp.ssreflect.bigop.html#NatConst">NatConst</a> [section, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#NatConst.A">NatConst.A</a> [variable, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#NatConst.I">NatConst.I</a> [variable, in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> -<a href="mathcomp.field.closed_field.html#natmulpT">natmulpT</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> <a href="mathcomp.ssreflect.seq.html#natnseq0P">natnseq0P</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.prime.html#NatPreds">NatPreds</a> [section, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.ssreflect.prime.html#NatPreds.n">NatPreds.n</a> [variable, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> @@ -519,10 +518,10 @@ <a href="mathcomp.ssreflect.ssrnat.html#NatTrec.oddE">NatTrec.oddE</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#NatTrec.oddn">NatTrec.oddn</a> [abbreviation, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#NatTrec.trecE">NatTrec.trecE</a> [definition, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#9ea91de45bbac2f7bc67d6bfcbe695b2">_ .*2 (nat_scope)</a> [notation, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#5324a05440e2ec11a1246af1f549ecf5">_ ^ _ (nat_scope)</a> [notation, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#db68ec9399320f6b1e74e6c173769d9a">_ * _ (nat_scope)</a> [notation, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#c50bd965cea0fa974be322ff7c9fa45b">_ + _ (nat_scope)</a> [notation, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#32e6860b865cd7b092dd7c4a60fccddf">_ .*2 (nat_scope)</a> [notation, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#374b5d4cfa228f716828011aba8078bb">_ ^ _ (nat_scope)</a> [notation, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#b45df11e8227e0b39aed62233ce88e3a">_ * _ (nat_scope)</a> [notation, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#2c676bc9fadf29ec192d19a5bb3692e3">_ + _ (nat_scope)</a> [notation, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.algebra.ssrint.html#natz">natz</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> <a href="mathcomp.ssreflect.prime.html#nat_pred">nat_pred</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> <a href="mathcomp.ssreflect.choice.html#nat_countMixin">nat_countMixin</a> [definition, in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/> @@ -534,8 +533,9 @@ <a href="mathcomp.ssreflect.ssrnat.html#nat_of_exp_bin">nat_of_exp_bin</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#nat_of_mul_bin">nat_of_mul_bin</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#nat_of_add_bin">nat_of_add_bin</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#nat_of_addn_gt0">nat_of_addn_gt0</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> -<a href="mathcomp.ssreflect.ssrnat.html#nat_of_succ_gt0">nat_of_succ_gt0</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#nat_of_mul_pos">nat_of_mul_pos</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#nat_of_add_pos">nat_of_add_pos</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#nat_of_succ_pos">nat_of_succ_pos</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#nat_of_binK">nat_of_binK</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#nat_of_pos">nat_of_pos</a> [definition, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.ssrnat.html#nat_AGM2">nat_AGM2</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> @@ -611,6 +611,8 @@ <a href="mathcomp.ssreflect.path.html#next_at">next_at</a> [definition, in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#nG">nG</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#nG">nG</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#nhomo_inj_lt_in">nhomo_inj_lt_in</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> +<a href="mathcomp.ssreflect.ssrnat.html#nhomo_inj_lt">nhomo_inj_lt</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.seq.html#Nil">Nil</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#nilP">nilP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#nilp">nilp</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -664,6 +666,26 @@ <a href="mathcomp.algebra.ssrint.html#nmulrz_lgt0">nmulrz_lgt0</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> <a href="mathcomp.algebra.matrix.html#nonconform_mx">nonconform_mx</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> <a href="mathcomp.character.integral_char.html#nonlinear_irr_vanish">nonlinear_irr_vanish</a> [lemma, in <a href="mathcomp.character.integral_char.html">mathcomp.character.integral_char</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType">NonPropType</a> [module, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.call">NonPropType.call</a> [definition, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.Call">NonPropType.Call</a> [constructor, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.callee">NonPropType.callee</a> [projection, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.call_of">NonPropType.call_of</a> [record, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.check">NonPropType.check</a> [definition, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.Check">NonPropType.Check</a> [constructor, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.condition">NonPropType.condition</a> [projection, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.Exports">NonPropType.Exports</a> [module, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.Exports.nonPropType">NonPropType.Exports.nonPropType</a> [abbreviation, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.Exports.notProp">NonPropType.Exports.notProp</a> [abbreviation, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.frame">NonPropType.frame</a> [projection, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.maybeProp">NonPropType.maybeProp</a> [definition, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.result">NonPropType.result</a> [projection, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.test">NonPropType.test</a> [projection, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.Test">NonPropType.Test</a> [constructor, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.test_negative">NonPropType.test_negative</a> [definition, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.test_Prop">NonPropType.test_Prop</a> [definition, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.test_of">NonPropType.test_of</a> [record, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> +<a href="mathcomp.ssreflect.ssreflect.html#NonPropType.type">NonPropType.type</a> [record, in <a href="mathcomp.ssreflect.ssreflect.html">mathcomp.ssreflect.ssreflect</a>]<br/> <a href="mathcomp.solvable.sylow.html#nontrivial_gacent_pgroup">nontrivial_gacent_pgroup</a> [lemma, in <a href="mathcomp.solvable.sylow.html">mathcomp.solvable.sylow</a>]<br/> <a href="mathcomp.field.fieldext.html#nonzero1fx">nonzero1fx</a> [lemma, in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/> <a href="mathcomp.algebra.rat.html#nonzero1q">nonzero1q</a> [lemma, in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/> @@ -808,6 +830,7 @@ <a href="mathcomp.ssreflect.tuple.html#nseq_tupleP">nseq_tupleP</a> [lemma, in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/> <a href="mathcomp.ssreflect.seq.html#nth">nth</a> [abbreviation, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#nth">nth</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#nthK">nthK</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#nthP">nthP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#NthTheory">NthTheory</a> [section, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#NthTheory.T">NthTheory.T</a> [variable, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -919,8 +942,8 @@ <a href="mathcomp.algebra.ssrnum.html#Num.ArchimedeanField.Exports">Num.ArchimedeanField.Exports</a> [module, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.ArchimedeanField.Exports.ArchiFieldType">Num.ArchimedeanField.Exports.ArchiFieldType</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.ArchimedeanField.Exports.archiFieldType">Num.ArchimedeanField.Exports.archiFieldType</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#a58841a2b4844911030c30bfa80595e1">[ archiFieldType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#d70ca3cc0dfddd155fdca7bda79af694">[ archiFieldType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#1d223ecefdc2e9e5b1ff24bb5389842d">[ archiFieldType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#e784f599516bacfb6b7d41bbe46c5124">[ archiFieldType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.ArchimedeanField.fieldType">Num.ArchimedeanField.fieldType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.ArchimedeanField.idomainType">Num.ArchimedeanField.idomainType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.ArchimedeanField.numDomainType">Num.ArchimedeanField.numDomainType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -959,8 +982,8 @@ <a href="mathcomp.algebra.ssrnum.html#Num.ClosedField.Exports">Num.ClosedField.Exports</a> [module, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.ClosedField.Exports.NumClosedFieldType">Num.ClosedField.Exports.NumClosedFieldType</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.ClosedField.Exports.numClosedFieldType">Num.ClosedField.Exports.numClosedFieldType</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#f35f0142f80d163945beb05160d401d5">[ numClosedFieldType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#53405ca907938fed833c1fec5ac3d770">[ numClosedFieldType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#2c47ec6cd511d79c480d7bbbc8275b5c">[ numClosedFieldType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#255a4f754e7d5b6785ffc09cef3daa45">[ numClosedFieldType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.ClosedField.fieldType">Num.ClosedField.fieldType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.ClosedField.idomainType">Num.ClosedField.idomainType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.ClosedField.imaginary">Num.ClosedField.imaginary</a> [projection, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -983,8 +1006,8 @@ <a href="mathcomp.algebra.ssrnum.html#Num.ClosedField.zmodType">Num.ClosedField.zmodType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Def">Num.Def</a> [module, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Def.Def">Num.Def.Def</a> [section, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#e24e94b919f2f836c2c853c0a739656b">_ < _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#2038926f673d4ab3e13573d88721ef3c">_ <= _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#59c6a70ef9ba684b2656037172ca179b">_ < _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#e8ef13454f83374e99578f4be43cfcc5">_ <= _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Def.ger">Num.Def.ger</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Def.gtr">Num.Def.gtr</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Def.ler">Num.Def.ler</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1082,8 +1105,8 @@ <a href="mathcomp.algebra.ssrnum.html#Num.NumDomain.Exports.NumDomainType">Num.NumDomain.Exports.NumDomainType</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.NumDomain.Exports.numDomainType">Num.NumDomain.Exports.numDomainType</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.NumDomain.Exports.NumMixin">Num.NumDomain.Exports.NumMixin</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#faa7b03f15fa8c0b383b6f3802b37e9e">[ numDomainType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#dfa3a41435329603f4a41bbb73d70957">[ numDomainType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#8bf783530208799b469bca451a6c1096">[ numDomainType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#baf407b71864fa921583b0a5bcec211a">[ numDomainType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.NumDomain.idomainType">Num.NumDomain.idomainType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.NumDomain.mixin">Num.NumDomain.mixin</a> [projection, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.NumDomain.pack">Num.NumDomain.pack</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1110,7 +1133,7 @@ <a href="mathcomp.algebra.ssrnum.html#Num.NumField.eqType">Num.NumField.eqType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.NumField.Exports">Num.NumField.Exports</a> [module, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.NumField.Exports.numFieldType">Num.NumField.Exports.numFieldType</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#a7441f0a0e6a98d4d20f782d49891896">[ numFieldType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#26b4c9111e913c6e720e7f07f31d3386">[ numFieldType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.NumField.fieldType">Num.NumField.fieldType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.NumField.idomainType">Num.NumField.idomainType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.NumField.join_numDomainType">Num.NumField.join_numDomainType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1145,8 +1168,8 @@ <a href="mathcomp.algebra.ssrnum.html#Num.RealClosedField.Exports">Num.RealClosedField.Exports</a> [module, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealClosedField.Exports.RcfType">Num.RealClosedField.Exports.RcfType</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealClosedField.Exports.rcfType">Num.RealClosedField.Exports.rcfType</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#489355e4822051a37f16f0d65e2778f8">[ rcfType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#d55f7ab3d406a321aadc0a2e4311d80c">[ rcfType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#91a87a2c615b521b2b9d16585efd598b">[ rcfType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#b31d1160b1445c26f71a3da39ff1bae8">[ rcfType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealClosedField.fieldType">Num.RealClosedField.fieldType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealClosedField.idomainType">Num.RealClosedField.idomainType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealClosedField.numDomainType">Num.RealClosedField.numDomainType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1178,8 +1201,8 @@ <a href="mathcomp.algebra.ssrnum.html#Num.RealDomain.Exports">Num.RealDomain.Exports</a> [module, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealDomain.Exports.RealDomainType">Num.RealDomain.Exports.RealDomainType</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealDomain.Exports.realDomainType">Num.RealDomain.Exports.realDomainType</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#0df319535c5b2c7df349bac58e95e96c">[ realDomainType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#97348e7f29e06cbe2672c3f0899ae4cb">[ realDomainType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#e6fcf6ae21d670095438210f8dc4a697">[ realDomainType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#9358ff9186f7d83e540a65a7a8e8c5a4">[ realDomainType of _ for _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealDomain.idomainType">Num.RealDomain.idomainType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealDomain.numDomainType">Num.RealDomain.numDomainType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealDomain.pack">Num.RealDomain.pack</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1206,10 +1229,11 @@ <a href="mathcomp.algebra.ssrnum.html#Num.RealField.eqType">Num.RealField.eqType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealField.Exports">Num.RealField.Exports</a> [module, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealField.Exports.realFieldType">Num.RealField.Exports.realFieldType</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#9bd0f21dc8f37cb47d141588c0e6729b">[ realFieldType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#d2e4c806361a8ca8b358ecd4af030445">[ realFieldType of _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealField.fieldType">Num.RealField.fieldType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealField.idomainType">Num.RealField.idomainType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.RealField.join_realDomainType">Num.RealField.join_realDomainType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.RealField.join_numFieldType">Num.RealField.join_numFieldType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.RealField.join_fieldType">Num.RealField.join_fieldType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealField.mixin">Num.RealField.mixin</a> [projection, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealField.numDomainType">Num.RealField.numDomainType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealField.numFieldType">Num.RealField.numFieldType</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1264,9 +1288,9 @@ <a href="mathcomp.algebra.ssrnum.html#Num.RealMixin.RealMixins.LtMixin.sub_gt0">Num.RealMixin.RealMixins.LtMixin.sub_gt0</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealMixin.RealMixins.norm">Num.RealMixin.RealMixins.norm</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealMixin.RealMixins.R">Num.RealMixin.RealMixins.R</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#de7043ea17a224ebc5072aadb91ca5c8">`| _ | (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#6742b89c3f5ac60b756597eec71a6ec6">_ < _</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#982e7680c015af99a74da7cd6b581a82">_ <= _</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#7a643e3755d4456d5e0ed76298231c3f">`| _ | (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#03f704784a37817b116d2da880d2b7d2">_ < _</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#8e511c48af27cf3689f1bf6fda0d102c">_ <= _</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.RealMixin.sub_ge0">Num.RealMixin.sub_ge0</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.real_closed_axiom">Num.real_closed_axiom</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.real_axiom">Num.real_axiom</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1274,34 +1298,34 @@ <a href="mathcomp.algebra.ssrnum.html#Num.sg">Num.sg</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.sqrt">Num.sqrt</a> [abbreviation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Syntax">Num.Syntax</a> [module, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#6019ab7c51b05c9f67093b53d0c48454">_ <= _ ?= iff _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#79bf01a504ffcda65f8e3d816a5515cd">_ <= _ ?= iff _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#7cd47ea66f219bc403cc6631c817f8b3">_ < _ < _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#93a29a58d1f90b8a91702885cf86161e">_ <= _ < _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#cbae941009021cd5693066355a023dd1">_ < _ <= _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#ff736a21b738c796d1200c3222013b46">_ <= _ <= _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#3975356ead321cf4577de4738f745485">_ >= _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#4a55c8439dfd5912be472b2910ab4015">_ >= _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#d6cd0798ccf4decf11598a746ae90abf">_ <= _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495">_ <= _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#f54d2e0a46f272d0295ade87cec65608">_ > _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#07bcd9d86ae6b6828fbc17b15193853f">_ > _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#3c0e77197870a42e4951057d43bba909">_ < _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b">_ < _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#6f89ccb02a8f0a5ad1eea6160e3c21ef">>= _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#23c398dbba06a0aa4819b2d9e2ed5abb">>= _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#13d5330a4568f6ceffcf63013bcd1f20"><= _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#e1cffdfd4384e2a91d841324fdf3cf74"><= _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#cbbb7fa9128771701eefac0819f9b044">> _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#a5bfa1108ca863ae15611f2aac402243">> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#59d3ae83284e7d320c78efee96f330f6">< _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#a8f34bc5e467f7971380049ef258ede0">< _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#6fd1556fdb6e0b11ebd82189f1bfb36f"><?=%R (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#186aaf7909c11e850d63c2993181ccc7">>=%R (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#81937a94685a0487cf97a240746fb002"><=%R (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#4f222b0e87b56a0bb524cc002c4daf40">>%R (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#1d9613d915748583958d042a98aee792"><%R (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#c536f9a86d3c053391521360ac3f5a61">`| _ | (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#9cd60a0d32a7e406c15fd6cd6625a3bc">_ <= _ ?= iff _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#8f3b4963db7e39cb42e593806a8ca50e">_ <= _ ?= iff _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#086ddf2c88f1fedcc119aa72d37c1c8d">_ < _ < _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#eecc969a2fa3156b5b7024f4c30ed163">_ <= _ < _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#2204180cdceca384f1146e14bfad202d">_ < _ <= _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#5285549f1bd0c3f181a17cc59d549bc0">_ <= _ <= _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#865c57092db77d0dd2beca87eeb15048">_ >= _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#a3446a989be902579d41cbac1597f4cf">_ >= _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#ba5152cc8b7dbce43c273ac9c15cfb7c">_ <= _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#cb42ec59ad57b25928e1718b4e69e031">_ <= _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#2ea6b0fa5012a58d9f4f8b861fb14ee8">_ > _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#1f96a77ded31d6d5fa0c8fe9a087652a">_ > _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#292c223180a62926ca0f2279c23ce13c">_ < _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#eb5186e6835d7e27cbb4c691b2f398bb">_ < _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#fe16df4ac4152b109435498606033424">>= _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#c36d1dabbd97a475f06cbfd8e0210bfa">>= _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#95738f4c769ddbd4a51f601be6ba85ea"><= _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#33c6bbcbdfcebbedf70279be2f5c58b4"><= _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#6884c7c75216aebd4ac0b38b290804ae">> _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#05f307680bec629a08f7d05dde61567b">> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#6edd09f961a5dce9142e69ba3c3a91e7">< _ :> _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#131b1a10ebee3efa5fc963f49ab399ec">< _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#a112602bf80a2c1be0e7b26a54f164d8"><?=%R (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#b1ad3c958dc3661480f281516715fa65">>=%R (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#3643037e980cd7437d5177a70fb7df6f"><=%R (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#59be59e16bad587ac1ecdb1174cfec66">>%R (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#bb60fb64ba2313b3f8bcefd06a90c9a6"><%R (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#55297ec87c6b3f98c14c99daeafb55d3">`| _ | (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory">Num.Theory</a> [module, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.addC_rect">Num.Theory.addC_rect</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.addr_maxr">Num.Theory.addr_maxr</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1318,6 +1342,10 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ArchimedeanFieldTheory.x">Num.Theory.ArchimedeanFieldTheory.x</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.archi_boundP">Num.Theory.archi_boundP</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.argCle">Num.Theory.argCle</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.arg_maxrP">Num.Theory.arg_maxrP</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.arg_minrP">Num.Theory.arg_minrP</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.arg_maxr">Num.Theory.arg_maxr</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.arg_minr">Num.Theory.arg_minr</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.Cauchy_root_bound">Num.Theory.Cauchy_root_bound</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.char_num">Num.Theory.char_num</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ClosedFieldTheory">Num.Theory.ClosedFieldTheory</a> [section, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1326,10 +1354,10 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ClosedFieldTheory.neg_unity_root">Num.Theory.ClosedFieldTheory.neg_unity_root</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ClosedFieldTheory.nz2">Num.Theory.ClosedFieldTheory.nz2</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ClosedFieldTheory.Re2">Num.Theory.ClosedFieldTheory.Re2</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#03c300d501fea655f6f62a3c297714e9">'Im _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#dcb39ac1261bac8232156a37fb17d31c">'Re _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#27eefe7225317752adf12d2ec6054502">_ .-root (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#faffc7ebdc59e33c8506558c91f1ae94">_ .-root (ring_core_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#736613b7caf3683df2a687c15a0f24d8">'Im _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#99dbca8152e41aef3613112680dd825c">'Re _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#d19e1425037436a9509238888bdd6655">_ .-root (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#3f3015d4b89b022dd77e42226683390f">_ .-root (ring_core_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.comparer">Num.Theory.comparer</a> [inductive, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ComparerEq">Num.Theory.ComparerEq</a> [constructor, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ComparerEq0">Num.Theory.ComparerEq0</a> [constructor, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1357,6 +1385,12 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.Creal_Im">Num.Theory.Creal_Im</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.Creal_Re">Num.Theory.Creal_Re</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.Crect">Num.Theory.Crect</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.decnr_inj_inj_in">Num.Theory.decnr_inj_inj_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.decnr_inj_inj">Num.Theory.decnr_inj_inj</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.decrn_inj_in">Num.Theory.decrn_inj_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.decrn_inj">Num.Theory.decrn_inj</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.decr_inj_in">Num.Theory.decr_inj_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.decr_inj">Num.Theory.decr_inj</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.distrC">Num.Theory.distrC</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.divr_gt0">Num.Theory.divr_gt0</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.divr_ge0">Num.Theory.divr_ge0</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1446,12 +1480,6 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.gtr0_real">Num.Theory.gtr0_real</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.gtr0_norm">Num.Theory.gtr0_norm</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.gt0_cp">Num.Theory.gt0_cp</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.homo_mono_in">Num.Theory.homo_mono_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.homo_mono">Num.Theory.homo_mono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.homo_leq_mono">Num.Theory.homo_leq_mono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.homo_inj_ltn_lt">Num.Theory.homo_inj_ltn_lt</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.homo_inj_in_lt">Num.Theory.homo_inj_in_lt</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.homo_inj_lt">Num.Theory.homo_inj_lt</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ieexprIn">Num.Theory.ieexprIn</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ieexprn_weq1">Num.Theory.ieexprn_weq1</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.Im">Num.Theory.Im</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1464,6 +1492,24 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.Im_conj">Num.Theory.Im_conj</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.Im_i">Num.Theory.Im_i</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.Im_is_additive">Num.Theory.Im_is_additive</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.incnr_inj_in">Num.Theory.incnr_inj_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.incnr_inj">Num.Theory.incnr_inj</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.incrn_inj_in">Num.Theory.incrn_inj_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.incrn_inj">Num.Theory.incrn_inj</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.incr_inj_in">Num.Theory.incr_inj_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.incr_inj">Num.Theory.incr_inj</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_nhomo_ltrn_in">Num.Theory.inj_nhomo_ltrn_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_homo_ltrn_in">Num.Theory.inj_homo_ltrn_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_nhomo_ltrn">Num.Theory.inj_nhomo_ltrn</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_homo_ltrn">Num.Theory.inj_homo_ltrn</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_nhomo_ltnr_in">Num.Theory.inj_nhomo_ltnr_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_homo_ltnr_in">Num.Theory.inj_homo_ltnr_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_nhomo_ltnr">Num.Theory.inj_nhomo_ltnr</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_homo_ltnr">Num.Theory.inj_homo_ltnr</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_nhomo_ltr_in">Num.Theory.inj_nhomo_ltr_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_homo_ltr_in">Num.Theory.inj_homo_ltr_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_nhomo_ltr">Num.Theory.inj_nhomo_ltr</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.inj_homo_ltr">Num.Theory.inj_homo_ltr</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.invCi">Num.Theory.invCi</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.invC_rect">Num.Theory.invC_rect</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.invC_norm">Num.Theory.invC_norm</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1492,10 +1538,14 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.IsSqrtr">Num.Theory.IsSqrtr</a> [constructor, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.lef_ninv">Num.Theory.lef_ninv</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.lef_pinv">Num.Theory.lef_pinv</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.leq_lerW_nmono">Num.Theory.leq_lerW_nmono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.leq_lerW_mono">Num.Theory.leq_lerW_mono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.leq_nmono_inj">Num.Theory.leq_nmono_inj</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.leq_mono_inj">Num.Theory.leq_mono_inj</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lenrW_nmono_in">Num.Theory.lenrW_nmono_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lenrW_mono_in">Num.Theory.lenrW_mono_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lenrW_nmono">Num.Theory.lenrW_nmono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lenrW_mono">Num.Theory.lenrW_mono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lenr_nmono_in">Num.Theory.lenr_nmono_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lenr_mono_in">Num.Theory.lenr_mono_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lenr_nmono">Num.Theory.lenr_nmono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lenr_mono">Num.Theory.lenr_mono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.lerifP">Num.Theory.lerifP</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.lerif_rootC_AGM">Num.Theory.lerif_rootC_AGM</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.lerif_Re_Creal">Num.Theory.lerif_Re_Creal</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1521,6 +1571,14 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.lerif_refl">Num.Theory.lerif_refl</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.lerNgt">Num.Theory.lerNgt</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.LerNotGt">Num.Theory.LerNotGt</a> [constructor, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lernW_nmono_in">Num.Theory.lernW_nmono_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lernW_mono_in">Num.Theory.lernW_mono_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lernW_nmono">Num.Theory.lernW_nmono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lernW_mono">Num.Theory.lernW_mono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lern_nmono_in">Num.Theory.lern_nmono_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lern_mono_in">Num.Theory.lern_mono_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lern_nmono">Num.Theory.lern_nmono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.lern_mono">Num.Theory.lern_mono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.lern0">Num.Theory.lern0</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.lern1">Num.Theory.lern1</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.lerN10">Num.Theory.lerN10</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1545,6 +1603,10 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_normlP">Num.Theory.ler_normlP</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_norml">Num.Theory.ler_norml</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_norm">Num.Theory.ler_norm</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_nmono_in">Num.Theory.ler_nmono_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_mono_in">Num.Theory.ler_mono_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_nmono">Num.Theory.ler_nmono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_mono">Num.Theory.ler_mono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_total">Num.Theory.ler_total</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_ndivr_mull">Num.Theory.ler_ndivr_mull</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ler_ndivl_mull">Num.Theory.ler_ndivl_mull</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1695,12 +1757,18 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.lter01">Num.Theory.lter01</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltf_ninv">Num.Theory.ltf_ninv</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltf_pinv">Num.Theory.ltf_pinv</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltn_ltrW_nhomo">Num.Theory.ltn_ltrW_nhomo</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltn_ltrW_homo">Num.Theory.ltn_ltrW_homo</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltnrW_nhomo_in">Num.Theory.ltnrW_nhomo_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltnrW_homo_in">Num.Theory.ltnrW_homo_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltnrW_nhomo">Num.Theory.ltnrW_nhomo</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltnrW_homo">Num.Theory.ltnrW_homo</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrgtP">Num.Theory.ltrgtP</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrgt0P">Num.Theory.ltrgt0P</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrNge">Num.Theory.ltrNge</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.LtrNotGe">Num.Theory.LtrNotGe</a> [constructor, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrnW_nhomo_in">Num.Theory.ltrnW_nhomo_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrnW_homo_in">Num.Theory.ltrnW_homo_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrnW_nhomo">Num.Theory.ltrnW_nhomo</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrnW_homo">Num.Theory.ltrnW_homo</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrn0">Num.Theory.ltrn0</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrn1">Num.Theory.ltrn1</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltrN10">Num.Theory.ltrN10</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1787,8 +1855,8 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_add">Num.Theory.ltr_add</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_le_add">Num.Theory.ltr_le_add</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_add2">Num.Theory.ltr_add2</a> [definition, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_add2l">Num.Theory.ltr_add2l</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_add2r">Num.Theory.ltr_add2r</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_add2l">Num.Theory.ltr_add2l</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_xor_ge">Num.Theory.ltr_xor_ge</a> [inductive, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_oppl">Num.Theory.ltr_oppl</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.ltr_oppr">Num.Theory.ltr_oppr</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1866,8 +1934,6 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.monic_Cauchy_bound">Num.Theory.monic_Cauchy_bound</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.mono_lerif">Num.Theory.mono_lerif</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.mono_in_lerif">Num.Theory.mono_in_lerif</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.mono_inj_in">Num.Theory.mono_inj_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.mono_inj">Num.Theory.mono_inj</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.mulC_rect">Num.Theory.mulC_rect</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.mulrIn">Num.Theory.mulrIn</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.mulrn_wlt0">Num.Theory.mulrn_wlt0</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1909,16 +1975,8 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.neqr0_sign">Num.Theory.neqr0_sign</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.neq0Ci">Num.Theory.neq0Ci</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.neq0_mulr_lt0">Num.Theory.neq0_mulr_lt0</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nhomo_mono_in">Num.Theory.nhomo_mono_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nhomo_mono">Num.Theory.nhomo_mono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nhomo_leq_mono">Num.Theory.nhomo_leq_mono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nhomo_inj_ltn_lt">Num.Theory.nhomo_inj_ltn_lt</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nhomo_inj_in_lt">Num.Theory.nhomo_inj_in_lt</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nhomo_inj_lt">Num.Theory.nhomo_inj_lt</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.nmono_lerif">Num.Theory.nmono_lerif</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.nmono_in_lerif">Num.Theory.nmono_in_lerif</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nmono_inj_in">Num.Theory.nmono_inj_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#Num.Theory.nmono_inj">Num.Theory.nmono_inj</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.nmulrn_rle0">Num.Theory.nmulrn_rle0</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.nmulrn_rge0">Num.Theory.nmulrn_rge0</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.nmulrn_rgt0">Num.Theory.nmulrn_rgt0</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1985,6 +2043,7 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumDomainMonotonyTheoryForReals">Num.Theory.NumDomainMonotonyTheoryForReals</a> [section, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumDomainMonotonyTheoryForReals.D">Num.Theory.NumDomainMonotonyTheoryForReals.D</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumDomainMonotonyTheoryForReals.f">Num.Theory.NumDomainMonotonyTheoryForReals.f</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumDomainMonotonyTheoryForReals.f'">Num.Theory.NumDomainMonotonyTheoryForReals.f'</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumDomainMonotonyTheoryForReals.R">Num.Theory.NumDomainMonotonyTheoryForReals.R</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumDomainMonotonyTheoryForReals.R'">Num.Theory.NumDomainMonotonyTheoryForReals.R'</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumDomainOperationTheory">Num.Theory.NumDomainOperationTheory</a> [section, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -1998,9 +2057,30 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.AcrossTypes.D">Num.Theory.NumIntegralDomainMonotonyTheory.AcrossTypes.D</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.AcrossTypes.D'">Num.Theory.NumIntegralDomainMonotonyTheory.AcrossTypes.D'</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.AcrossTypes.f">Num.Theory.NumIntegralDomainMonotonyTheory.AcrossTypes.f</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.geq_total">Num.Theory.NumIntegralDomainMonotonyTheory.geq_total</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.geq_anti">Num.Theory.NumIntegralDomainMonotonyTheory.geq_anti</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.ger_antiR'">Num.Theory.NumIntegralDomainMonotonyTheory.ger_antiR'</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.ger_antiR">Num.Theory.NumIntegralDomainMonotonyTheory.ger_antiR</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.gtnE">Num.Theory.NumIntegralDomainMonotonyTheory.gtnE</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.gtrE">Num.Theory.NumIntegralDomainMonotonyTheory.gtrE</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.gtr'E">Num.Theory.NumIntegralDomainMonotonyTheory.gtr'E</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.leqnn">Num.Theory.NumIntegralDomainMonotonyTheory.leqnn</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.leq_total">Num.Theory.NumIntegralDomainMonotonyTheory.leq_total</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.leq_anti">Num.Theory.NumIntegralDomainMonotonyTheory.leq_anti</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.ler_antiR'">Num.Theory.NumIntegralDomainMonotonyTheory.ler_antiR'</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.ler_antiR">Num.Theory.NumIntegralDomainMonotonyTheory.ler_antiR</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.ltnE">Num.Theory.NumIntegralDomainMonotonyTheory.ltnE</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.ltrE">Num.Theory.NumIntegralDomainMonotonyTheory.ltrE</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.ltr'E">Num.Theory.NumIntegralDomainMonotonyTheory.ltr'E</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.NatToR">Num.Theory.NumIntegralDomainMonotonyTheory.NatToR</a> [section, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.NatToR.D">Num.Theory.NumIntegralDomainMonotonyTheory.NatToR.D</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.NatToR.D'">Num.Theory.NumIntegralDomainMonotonyTheory.NatToR.D'</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.NatToR.f">Num.Theory.NumIntegralDomainMonotonyTheory.NatToR.f</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.R">Num.Theory.NumIntegralDomainMonotonyTheory.R</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.RToNat">Num.Theory.NumIntegralDomainMonotonyTheory.RToNat</a> [section, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.RToNat.D">Num.Theory.NumIntegralDomainMonotonyTheory.RToNat.D</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.RToNat.D'">Num.Theory.NumIntegralDomainMonotonyTheory.RToNat.D'</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.RToNat.f">Num.Theory.NumIntegralDomainMonotonyTheory.RToNat.f</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainMonotonyTheory.R'">Num.Theory.NumIntegralDomainMonotonyTheory.R'</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainTheory">Num.Theory.NumIntegralDomainTheory</a> [section, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.NumIntegralDomainTheory.R">Num.Theory.NumIntegralDomainTheory.R</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -2053,9 +2133,11 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.RealClosedFieldTheory">Num.Theory.RealClosedFieldTheory</a> [section, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.RealClosedFieldTheory.R">Num.Theory.RealClosedFieldTheory.R</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.realD">Num.Theory.realD</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.RealDomainArgExtremum">Num.Theory.RealDomainArgExtremum</a> [section, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.RealDomainMonotony">Num.Theory.RealDomainMonotony</a> [section, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.RealDomainMonotony.D">Num.Theory.RealDomainMonotony.D</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.RealDomainMonotony.f">Num.Theory.RealDomainMonotony.f</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.RealDomainMonotony.f'">Num.Theory.RealDomainMonotony.f'</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.RealDomainMonotony.R">Num.Theory.RealDomainMonotony.R</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.RealDomainMonotony.R'">Num.Theory.RealDomainMonotony.R'</a> [variable, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.RealDomainOperations">Num.Theory.RealDomainOperations</a> [section, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -2078,6 +2160,10 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.realN">Num.Theory.realN</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.realn">Num.Theory.realn</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.realNEsign">Num.Theory.realNEsign</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.realn_nmono_in">Num.Theory.realn_nmono_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.realn_mono_in">Num.Theory.realn_mono_in</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.realn_nmono">Num.Theory.realn_nmono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#Num.Theory.realn_mono">Num.Theory.realn_mono</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.realrM">Num.Theory.realrM</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.realrMn">Num.Theory.realrMn</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.realV">Num.Theory.realV</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> @@ -2237,12 +2323,18 @@ <a href="mathcomp.algebra.ssrnum.html#Num.Theory.upper_nthrootP">Num.Theory.upper_nthrootP</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.wlog_ltr">Num.Theory.wlog_ltr</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.algebra.ssrnum.html#Num.Theory.wlog_ler">Num.Theory.wlog_ler</a> [lemma, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#581a18ced675f8f9c5eb585ba4ae312b">'Im _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#9153b7cf9b84603850c08e5131d1133a">'Re _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#f2048b82a608311baf565ccc9caefe54">'i (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#04479a6ff05539b339540fbd2eba4ebf">_ .-root (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#f2048b82a608311baf565ccc9caefe54">'i (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> -<a href="mathcomp.algebra.ssrnum.html#b07d6e6599ef6e468ce182ffe6029532">_ ^* (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#d096db684c472dab4df549257e1ff1d7">[ arg maxr_ ( _ > _ ) _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#5fe3247cb32b89fbe5aeeeada892756c">[ arg maxr_ ( _ > _ in _ ) _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#d0b789d0e6862b40cc910a9d227c2413">[ arg maxr_ ( _ > _ | _ ) _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#1b686660a6be196fa2eaeec0a2ad58f1">[ arg minr_ ( _ < _ ) _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#f3cd7a00f84cbf03c7e306cb3b7ad0cb">[ arg minr_ ( _ < _ in _ ) _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#06bf477c149957fa9134e5f78a765163">[ arg minr_ ( _ < _ | _ ) _ ] (form_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#e17db6da38f8f20b1006c3799708d2df">'Im _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#41f056fd884172371f967a4a9b1ae751">'Re _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#075696c58083c87c2cf84f5ae31b0cb0">'i (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#7aa9ce4a7f9454ba6539a8c1c168f107">_ .-root (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#075696c58083c87c2cf84f5ae31b0cb0">'i (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> +<a href="mathcomp.algebra.ssrnum.html#651a776cde67abfb8f7231c08f29d878">_ ^* (ring_scope)</a> [notation, in <a href="mathcomp.algebra.ssrnum.html">mathcomp.algebra.ssrnum</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#nz_socle">nz_socle</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.character.mxrepresentation.html#nz_row_mxsimple">nz_row_mxsimple</a> [lemma, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/> <a href="mathcomp.algebra.matrix.html#nz_row_eq0">nz_row_eq0</a> [lemma, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/> @@ -2290,7 +2382,7 @@ <td><a href="index_global_Z.html">Z</a></td> <td>_</td> <td><a href="index_global_*.html">other</a></td> -<td>(23233 entries)</td> +<td>(23836 entries)</td> </tr> <tr> <td>Notation Index</td> @@ -2322,14 +2414,14 @@ <td><a href="index_notation_Z.html">Z</a></td> <td>_</td> <td><a href="index_notation_*.html">other</a></td> -<td>(1373 entries)</td> +<td>(1409 entries)</td> </tr> <tr> <td>Module Index</td> <td><a href="index_module_A.html">A</a></td> <td><a href="index_module_B.html">B</a></td> <td><a href="index_module_C.html">C</a></td> -<td>D</td> +<td><a href="index_module_D.html">D</a></td> <td><a href="index_module_E.html">E</a></td> <td><a href="index_module_F.html">F</a></td> <td><a href="index_module_G.html">G</a></td> @@ -2354,7 +2446,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(213 entries)</td> +<td>(221 entries)</td> </tr> <tr> <td>Variable Index</td> @@ -2386,7 +2478,7 @@ <td><a href="index_variable_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(3475 entries)</td> +<td>(3574 entries)</td> </tr> <tr> <td>Library Index</td> @@ -2418,7 +2510,7 @@ <td><a href="index_library_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(89 entries)</td> +<td>(90 entries)</td> </tr> <tr> <td>Lemma Index</td> @@ -2450,7 +2542,7 @@ <td><a href="index_lemma_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(11853 entries)</td> +<td>(12096 entries)</td> </tr> <tr> <td>Constructor Index</td> @@ -2482,7 +2574,7 @@ <td><a href="index_constructor_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(359 entries)</td> +<td>(368 entries)</td> </tr> <tr> <td>Axiom Index</td> @@ -2514,7 +2606,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(47 entries)</td> +<td>(45 entries)</td> </tr> <tr> <td>Inductive Index</td> @@ -2546,14 +2638,14 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(103 entries)</td> +<td>(107 entries)</td> </tr> <tr> <td>Projection Index</td> <td><a href="index_projection_A.html">A</a></td> <td><a href="index_projection_B.html">B</a></td> <td><a href="index_projection_C.html">C</a></td> -<td>D</td> +<td><a href="index_projection_D.html">D</a></td> <td><a href="index_projection_E.html">E</a></td> <td><a href="index_projection_F.html">F</a></td> <td><a href="index_projection_G.html">G</a></td> @@ -2578,7 +2670,7 @@ <td><a href="index_projection_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(266 entries)</td> +<td>(273 entries)</td> </tr> <tr> <td>Section Index</td> @@ -2610,7 +2702,7 @@ <td><a href="index_section_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(1118 entries)</td> +<td>(1140 entries)</td> </tr> <tr> <td>Abbreviation Index</td> @@ -2642,7 +2734,7 @@ <td><a href="index_abbreviation_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(691 entries)</td> +<td>(728 entries)</td> </tr> <tr> <td>Definition Index</td> @@ -2674,14 +2766,14 @@ <td><a href="index_definition_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(3461 entries)</td> +<td>(3596 entries)</td> </tr> <tr> <td>Record Index</td> <td><a href="index_record_A.html">A</a></td> <td>B</td> <td><a href="index_record_C.html">C</a></td> -<td>D</td> +<td><a href="index_record_D.html">D</a></td> <td><a href="index_record_E.html">E</a></td> <td><a href="index_record_F.html">F</a></td> <td><a href="index_record_G.html">G</a></td> @@ -2706,7 +2798,7 @@ <td><a href="index_record_Z.html">Z</a></td> <td>_</td> <td>other</td> -<td>(185 entries)</td> +<td>(189 entries)</td> </tr> </table> </div> |