aboutsummaryrefslogtreecommitdiff
path: root/docs/htmldoc/index_global_I.html
diff options
context:
space:
mode:
authorEnrico Tassi2019-05-22 13:43:08 +0200
committerEnrico Tassi2019-05-22 15:34:14 +0200
commit748d716efb2f2f75946c8386e441ce1789806a39 (patch)
treefe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/index_global_I.html
parent415be3b908daadabf178a292c885db78e5b2c9a4 (diff)
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/index_global_I.html')
-rw-r--r--docs/htmldoc/index_global_I.html149
1 files changed, 74 insertions, 75 deletions
diff --git a/docs/htmldoc/index_global_I.html b/docs/htmldoc/index_global_I.html
index 8f948c3..95663cd 100644
--- a/docs/htmldoc/index_global_I.html
+++ b/docs/htmldoc/index_global_I.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_I"></a><h2>I </h2>
@@ -506,11 +506,6 @@
<a href="mathcomp.algebra.ssrint.html#ieexprIz">ieexprIz</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.fingroup.morphism.html#ifactm">ifactm</a> [definition, in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/>
<a href="mathcomp.fingroup.morphism.html#ifactmE">ifactmE</a> [lemma, in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#ifnz">ifnz</a> [definition, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#ifnzP">ifnzP</a> [lemma, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#IfnzPos">IfnzPos</a> [constructor, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#IfnzZero">IfnzZero</a> [constructor, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
-<a href="mathcomp.ssreflect.prime.html#ifnz_spec">ifnz_spec</a> [inductive, in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/>
<a href="mathcomp.ssreflect.eqtype.html#ifN_eqC">ifN_eqC</a> [lemma, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/>
<a href="mathcomp.ssreflect.eqtype.html#ifN_eq">ifN_eq</a> [lemma, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/>
<a href="mathcomp.character.mxrepresentation.html#iG">iG</a> [abbreviation, in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
@@ -632,6 +627,10 @@
<a href="mathcomp.solvable.cyclic.html#im_Zpm">im_Zpm</a> [lemma, in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/>
<a href="mathcomp.ssreflect.finset.html#im_transversal_repr">im_transversal_repr</a> [lemma, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/>
<a href="mathcomp.solvable.hall.html#inA">inA</a> [abbreviation, in <a href="mathcomp.solvable.hall.html">mathcomp.solvable.hall</a>]<br/>
+<a href="mathcomp.ssreflect.ssrnat.html#incrn_inj_in">incrn_inj_in</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
+<a href="mathcomp.ssreflect.ssrnat.html#incrn_inj">incrn_inj</a> [lemma, in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#incr_tallyP">incr_tallyP</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#incr_tally">incr_tally</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#incr_nthC">incr_nthC</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#incr_nth_inj">incr_nth_inj</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#incr_nth">incr_nth</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
@@ -686,11 +685,12 @@
<a href="mathcomp.character.character.html#Induced.H">Induced.H</a> [variable, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
<a href="mathcomp.character.classfun.html#Induced.H">Induced.H</a> [variable, in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
<a href="mathcomp.character.classfun.html#Induced.K">Induced.K</a> [variable, in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
-<a href="mathcomp.character.classfun.html#dbbc86b4ca58c3cba967ad32d9fc9e38">'Ind[ _ ] (ring_scope)</a> [notation, in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
-<a href="mathcomp.character.classfun.html#daddb95a75ea247d15dea0e3524a63e5">'Ind[ _ , _ ] (ring_scope)</a> [notation, in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
+<a href="mathcomp.character.classfun.html#bc3433d79d98cfd82a70b7d11c234953">'Ind[ _ ] (ring_scope)</a> [notation, in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
+<a href="mathcomp.character.classfun.html#ac99de1882838d8c0eab088180289562">'Ind[ _ , _ ] (ring_scope)</a> [notation, in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
<a href="mathcomp.character.character.html#Ind_Iirr">Ind_Iirr</a> [definition, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
<a href="mathcomp.character.character.html#Ind_irr_neq0">Ind_irr_neq0</a> [lemma, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#inE">inE</a> [definition, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
+<a href="mathcomp.ssreflect.ssrbool.html#inE">inE</a> [definition, in <a href="mathcomp.ssreflect.ssrbool.html">mathcomp.ssreflect.ssrbool</a>]<br/>
<a href="mathcomp.ssreflect.finset.html#inE">inE</a> [definition, in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/>
<a href="mathcomp.character.inertia.html#inertia">inertia</a> [definition, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
<a href="mathcomp.character.inertia.html#Inertia">Inertia</a> [section, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
@@ -752,11 +752,11 @@
<a href="mathcomp.character.inertia.html#Inertia.G">Inertia.G</a> [variable, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
<a href="mathcomp.character.inertia.html#Inertia.gT">Inertia.gT</a> [variable, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
<a href="mathcomp.character.inertia.html#Inertia.H">Inertia.H</a> [variable, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
-<a href="mathcomp.character.inertia.html#ddda694c2b3215cd89e224821b0146f2">_ ^: _ (cfun_scope)</a> [notation, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
-<a href="mathcomp.character.inertia.html#f2d45fe5e22876ae02944b97d4ededbb">'I_ _ [ _ ] (Group_scope)</a> [notation, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
-<a href="mathcomp.character.inertia.html#e4bb12f301df6a67d96a5924b209f783">'I[ _ ] (Group_scope)</a> [notation, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
-<a href="mathcomp.character.inertia.html#6a989a6414a722580f13fcad5931885d">'I_ _ [ _ ] (group_scope)</a> [notation, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
-<a href="mathcomp.character.inertia.html#99fa4ab272515ca96008d1110d766674">'I[ _ ] (group_scope)</a> [notation, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
+<a href="mathcomp.character.inertia.html#0df56e8239d8a380b545a76c4949b3d8">_ ^: _ (cfun_scope)</a> [notation, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
+<a href="mathcomp.character.inertia.html#f27d4db825c606ee5924a4a800c7620e">'I_ _ [ _ ] (Group_scope)</a> [notation, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
+<a href="mathcomp.character.inertia.html#075ad9b500a07b0781525b8078fb55ac">'I[ _ ] (Group_scope)</a> [notation, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
+<a href="mathcomp.character.inertia.html#d7868928c9838e25cd788c180bafc9d3">'I_ _ [ _ ] (group_scope)</a> [notation, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
+<a href="mathcomp.character.inertia.html#3ee2a1dd4ae14529933a33a195dedd6e">'I[ _ ] (group_scope)</a> [notation, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
<a href="mathcomp.character.inertia.html#inertia0">inertia0</a> [lemma, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
<a href="mathcomp.character.inertia.html#Inertia1">Inertia1</a> [lemma, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
<a href="mathcomp.character.inertia.html#inertia1">inertia1</a> [lemma, in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
@@ -772,9 +772,11 @@
<a href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.px_0">InfinitePrimitiveElementTheorem.px_0</a> [variable, in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
<a href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.x">InfinitePrimitiveElementTheorem.x</a> [variable, in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
<a href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.y">InfinitePrimitiveElementTheorem.y</a> [variable, in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
-<a href="mathcomp.field.separable.html#59212b1a12dae621b413316be212d437">_ ^ _ (ring_scope)</a> [notation, in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
+<a href="mathcomp.field.separable.html#38cc4a0ecff51aef123b4feb1fb0b274">_ ^ _ (ring_scope)</a> [notation, in <a href="mathcomp.field.separable.html">mathcomp.field.separable</a>]<br/>
<a href="mathcomp.solvable.hall.html#inG">inG</a> [abbreviation, in <a href="mathcomp.solvable.hall.html">mathcomp.solvable.hall</a>]<br/>
<a href="mathcomp.fingroup.action.html#inH">inH</a> [abbreviation, in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/>
+<a href="mathcomp.ssreflect.finfun.html#InheritedStructures">InheritedStructures</a> [section, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/>
+<a href="mathcomp.ssreflect.finfun.html#InheritedStructures.aT">InheritedStructures.aT</a> [variable, in <a href="mathcomp.ssreflect.finfun.html">mathcomp.ssreflect.finfun</a>]<br/>
<a href="mathcomp.algebra.intdiv.html#inIntSpan">inIntSpan</a> [definition, in <a href="mathcomp.algebra.intdiv.html">mathcomp.algebra.intdiv</a>]<br/>
<a href="mathcomp.ssreflect.fintype.html#injectiveb">injectiveb</a> [definition, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
<a href="mathcomp.ssreflect.fintype.html#Injectiveb">Injectiveb</a> [section, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
@@ -952,6 +954,8 @@
<a href="mathcomp.ssreflect.seq.html#inj_map">inj_map</a> [lemma, in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.fintype.html#inj_card_bij">inj_card_bij</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
<a href="mathcomp.ssreflect.fintype.html#inj_card_onto">inj_card_onto</a> [lemma, in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.eqtype.html#inj_homo">inj_homo</a> [lemma, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/>
+<a href="mathcomp.ssreflect.eqtype.html#inj_homo_in">inj_homo_in</a> [lemma, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/>
<a href="mathcomp.ssreflect.eqtype.html#inj_eqAxiom">inj_eqAxiom</a> [lemma, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/>
<a href="mathcomp.ssreflect.eqtype.html#inj_in_eq">inj_in_eq</a> [lemma, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/>
<a href="mathcomp.ssreflect.eqtype.html#inj_eq">inj_eq</a> [lemma, in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/>
@@ -1011,8 +1015,8 @@
<a href="mathcomp.algebra.ssrint.html#IntDist.leqif_add_distz">IntDist.leqif_add_distz</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#IntDist.leq_add_dist">IntDist.leq_add_dist</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#IntDist.sqrn_dist">IntDist.sqrn_dist</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#878788e4c3198d7431c2d18c9b6d439d">_ - _ (distn_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#521bb1f21db4ea2eead2a81dcc1b61f3">`| _ | (nat_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
+<a href="mathcomp.algebra.ssrint.html#5ba4b7527c38fa3e2d1321ab9def48d2">_ - _ (distn_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
+<a href="mathcomp.algebra.ssrint.html#124262c1d6731d26a230b737e0b3e9b6">`| _ | (nat_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.intdiv.html">intdiv</a> [library]<br/>
<a href="mathcomp.character.integral_char.html#IntegralChar">IntegralChar</a> [section, in <a href="mathcomp.character.integral_char.html">mathcomp.character.integral_char</a>]<br/>
<a href="mathcomp.character.integral_char.html#IntegralChar.G">IntegralChar.G</a> [variable, in <a href="mathcomp.character.integral_char.html">mathcomp.character.integral_char</a>]<br/>
@@ -1080,22 +1084,14 @@
<a href="mathcomp.algebra.interval.html#Interval">Interval</a> [constructor, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
<a href="mathcomp.algebra.interval.html#interval">interval</a> [inductive, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
<a href="mathcomp.algebra.interval.html">interval</a> [library]<br/>
+<a href="mathcomp.algebra.interval.html#IntervalEq">IntervalEq</a> [section, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
+<a href="mathcomp.algebra.interval.html#IntervalEq.T">IntervalEq.T</a> [variable, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
<a href="mathcomp.algebra.interval.html#IntervalField">IntervalField</a> [section, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
<a href="mathcomp.algebra.interval.html#IntervalField.R">IntervalField.R</a> [variable, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
<a href="mathcomp.algebra.interval.html#IntervalOrdered">IntervalOrdered</a> [section, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
<a href="mathcomp.algebra.interval.html#IntervalOrdered.R">IntervalOrdered.R</a> [variable, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
<a href="mathcomp.algebra.interval.html#IntervalPo">IntervalPo</a> [section, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
<a href="mathcomp.algebra.interval.html#IntervalPo.R">IntervalPo.R</a> [variable, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac">_ <= _ ?< if _ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#996170680ea33f9a35c3d01667d531c3">`] -oo , +oo [ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#ddab974cd5332360c70b1aca114bd394">`] _ , +oo [ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#84c6be04931432ed71a28392cd19d478">`[ _ , +oo [ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#f7d4545c39e6f558b751e487fae5aef4">`] -oo , _ [ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#6d014c3c0583cf03ab0a7cdc9d80e6e4">`] -oo , _ ] (ring_scope)</a> [notation, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#5d6177042cf2728bb3a48ad4d7fef36d">`] _ , _ [ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac">`[ _ , _ [ (ring_scope)</a> [notation, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09">`] _ , _ ] (ring_scope)</a> [notation, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
-<a href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af">`[ _ , _ ] (ring_scope)</a> [notation, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#intEsg">intEsg</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#intEsign">intEsign</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#intmul">intmul</a> [definition, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
@@ -1124,9 +1120,9 @@
<a href="mathcomp.algebra.ssrint.html#intRingTheory">intRingTheory</a> [section, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#intRing.comMixin">intRing.comMixin</a> [definition, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#intRing.intRing">intRing.intRing</a> [section, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#29f521e893e5de614d8a5fea63ebc756">_ * _ (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#c595220a1a12a506ce155bd2b4d32356">*%Z (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#1c55f52cd367a9786b56f9604686d38c">1 (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
+<a href="mathcomp.algebra.ssrint.html#01e4a35d9c55736d45586b343060db94">_ * _ (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
+<a href="mathcomp.algebra.ssrint.html#dfdaee88c459e64fbdba00f90ccc6d76">*%Z (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
+<a href="mathcomp.algebra.ssrint.html#6e5b82947260aa9ba9c9416d39c2ff3e">1 (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#intRing.mulNz">intRing.mulNz</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#intRing.mulz">intRing.mulz</a> [definition, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#intRing.mulzA">intRing.mulzA</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
@@ -1179,12 +1175,12 @@
<a href="mathcomp.algebra.ssrint.html#intZmod.add1Pz">intZmod.add1Pz</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#intZmod.intP">intZmod.intP</a> [lemma, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#intZmod.intZmod">intZmod.intZmod</a> [section, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#2553e52a52e348d7cd01529c54d5b3d8">_ - _ (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#d3ec034893cac385d2261c9b67bd46a4">_ + _ (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#16fe9c03523da4e4fa0c7bdd7e456ee3">+%Z (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#fd14de08ee988ca4bf75ec91ab30dd39">- _ (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#044e0a2bfc67e7b631e0b437110dfff4">-%Z (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
-<a href="mathcomp.algebra.ssrint.html#0fcbeb07e9d7998c7f0ccf8964c0dd31">0 (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
+<a href="mathcomp.algebra.ssrint.html#c3b69bd8c89d9288d1e3ced79b1d6121">_ - _ (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
+<a href="mathcomp.algebra.ssrint.html#7380c0bf0ef5fb884bf3a6f05fb9148b">_ + _ (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
+<a href="mathcomp.algebra.ssrint.html#8111b3af44b4af272208ad330faf5834">+%Z (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
+<a href="mathcomp.algebra.ssrint.html#41b3fe1175638847bc80590fe1102ffc">- _ (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
+<a href="mathcomp.algebra.ssrint.html#3f0573c91b4e7711ee58139ea565afe3">-%Z (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
+<a href="mathcomp.algebra.ssrint.html#d0fe8addb0b1166c9c68479395c2f797">0 (int_scope)</a> [notation, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#intZmod.int_spec">intZmod.int_spec</a> [inductive, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#intZmod.int_ind">intZmod.int_ind</a> [definition, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#intZmod.int_rec">intZmod.int_rec</a> [definition, in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
@@ -1338,9 +1334,9 @@
<a href="mathcomp.character.character.html#IrrClass.gT">IrrClass.gT</a> [variable, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
<a href="mathcomp.character.character.html#IrrClass.R_G">IrrClass.R_G</a> [variable, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
<a href="mathcomp.character.character.html#IrrClass.sG">IrrClass.sG</a> [variable, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#ec96925fba3f0715318b4e1d871abe75">'e_ _</a> [notation, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#f64cb7d496212396dd8e1623d34f269e">'n_ _</a> [notation, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
-<a href="mathcomp.character.character.html#3cfb4dcb4fb55ccb484b841cf32314ff">'R_ _</a> [notation, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
+<a href="mathcomp.character.character.html#a2283ad47979c7821fe6d70d159dc0f5">'e_ _</a> [notation, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
+<a href="mathcomp.character.character.html#8b022bdd3e8afd1d802a570e34363ef0">'n_ _</a> [notation, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
+<a href="mathcomp.character.character.html#49783294b9f6804d8e1991317fec1b3a">'R_ _</a> [notation, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
<a href="mathcomp.character.character.html#IrrConstt">IrrConstt</a> [section, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
<a href="mathcomp.character.character.html#IrrConstt.G">IrrConstt.G</a> [variable, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
<a href="mathcomp.character.character.html#IrrConstt.gT">IrrConstt.gT</a> [variable, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
@@ -1423,9 +1419,6 @@
<a href="mathcomp.character.character.html#IsChar.gT">IsChar.gT</a> [variable, in <a href="mathcomp.character.character.html">mathcomp.character.character</a>]<br/>
<a href="mathcomp.fingroup.fingroup.html#isgroupP">isgroupP</a> [lemma, in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
<a href="mathcomp.algebra.matrix.html#IsMxvecIndex">IsMxvecIndex</a> [constructor, in <a href="mathcomp.algebra.matrix.html">mathcomp.algebra.matrix</a>]<br/>
-<a href="mathcomp.field.closed_field.html#isnull">isnull</a> [definition, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#isnullP">isnullP</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#isnull_qf">isnull_qf</a> [lemma, in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
<a href="mathcomp.solvable.center.html#isob">isob</a> [abbreviation, in <a href="mathcomp.solvable.center.html">mathcomp.solvable.center</a>]<br/>
<a href="mathcomp.fingroup.morphism.html#IsoBoolEquiv">IsoBoolEquiv</a> [section, in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/>
<a href="mathcomp.fingroup.morphism.html#IsoBoolEquiv.G">IsoBoolEquiv.G</a> [variable, in <a href="mathcomp.fingroup.morphism.html">mathcomp.fingroup.morphism</a>]<br/>
@@ -1637,9 +1630,15 @@
<a href="mathcomp.ssreflect.fingraph.html#iter_in">iter_in</a> [lemma, in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/>
<a href="mathcomp.ssreflect.fingraph.html#iter_findex">iter_findex</a> [lemma, in <a href="mathcomp.ssreflect.fingraph.html">mathcomp.ssreflect.fingraph</a>]<br/>
<a href="mathcomp.algebra.interval.html#itvP">itvP</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
+<a href="mathcomp.algebra.interval.html#itv_intersectionA">itv_intersectionA</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
+<a href="mathcomp.algebra.interval.html#itv_intersectionC">itv_intersectionC</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
<a href="mathcomp.algebra.interval.html#itv_splitU2">itv_splitU2</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
<a href="mathcomp.algebra.interval.html#itv_splitU">itv_splitU</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
<a href="mathcomp.algebra.interval.html#itv_splitI">itv_splitI</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
+<a href="mathcomp.algebra.interval.html#itv_intersectionii">itv_intersectionii</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
+<a href="mathcomp.algebra.interval.html#itv_intersectioni1">itv_intersectioni1</a> [definition, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
+<a href="mathcomp.algebra.interval.html#itv_intersection1i">itv_intersection1i</a> [definition, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
+<a href="mathcomp.algebra.interval.html#itv_intersection">itv_intersection</a> [definition, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
<a href="mathcomp.algebra.interval.html#itv_gte">itv_gte</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
<a href="mathcomp.algebra.interval.html#itv_xx">itv_xx</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
<a href="mathcomp.algebra.interval.html#itv_boundlr">itv_boundlr</a> [lemma, in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/>
@@ -1678,7 +1677,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>
@@ -1710,14 +1709,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>
@@ -1742,7 +1741,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(213 entries)</td>
+<td>(221 entries)</td>
</tr>
<tr>
<td>Variable Index</td>
@@ -1774,7 +1773,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>
@@ -1806,7 +1805,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>
@@ -1838,7 +1837,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>
@@ -1870,7 +1869,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>
@@ -1902,7 +1901,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(47 entries)</td>
+<td>(45 entries)</td>
</tr>
<tr>
<td>Inductive Index</td>
@@ -1934,14 +1933,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>
@@ -1966,7 +1965,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>
@@ -1998,7 +1997,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>
@@ -2030,7 +2029,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>
@@ -2062,14 +2061,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>
@@ -2094,7 +2093,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>
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-09 09:44:24 +0000