-
Notifications
You must be signed in to change notification settings - Fork 11
Expand file tree
/
Copy pathindex.html
More file actions
412 lines (404 loc) · 46.4 KB
/
Copy pathindex.html
File metadata and controls
412 lines (404 loc) · 46.4 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
<!DOCTYPE html>
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Mathematical Components 7cde45af</title>
<meta name="description" content="Documentation of Coq module Mathematical Components 7cde45af" />
<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex/dist/katex.min.css">
<script src="https://cdn.jsdelivr.net/npm/markdown-it/dist/markdown-it.min.js"></script>
<script src="https://cdn.jsdelivr.net/npm/katex/dist/katex.min.js"></script>
<script src="https://cdn.jsdelivr.net/npm/markdown-it-texmath/texmath.min.js"></script>
<script src="https://cdn.jsdelivr.net/npm/darkmode-js@1.5.7/lib/darkmode-js.min.js"></script>
<link href="rocqnavi.css" rel="stylesheet" type="text/css" />
<script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.3.1/jquery.min.js"></script>
<script type="text/javascript" src="rocqnavi.js"> </script>
</head>
<body onload="init()">
<main>
<div class="sidebar">
<h2>Files</h2>
<li><details id="mathcomp"><summary>mathcomp</summary>
<ul>
<li><details id="mathcomp.algebra"><summary>algebra</summary>
<ul>
<li><details id="mathcomp.algebra.algebraic_hierarchy"><summary>algebraic_hierarchy</summary>
<ul>
<li><a href="mathcomp.algebra.algebraic_hierarchy.decfield.html">decfield</a></li>
<li><a href="mathcomp.algebra.algebraic_hierarchy.divalg.html">divalg</a></li>
<li><a href="mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras.html">rings_modules_and_algebras</a></li>
<li><a href="mathcomp.algebra.algebraic_hierarchy.ssralg.html">ssralg</a></li>
</ul>
</details>
</li>
<li><details id="mathcomp.algebra.numeric_hierarchy"><summary>numeric_hierarchy</summary>
<ul>
<li><a href="mathcomp.algebra.numeric_hierarchy.numdomain.html">numdomain</a></li>
<li><a href="mathcomp.algebra.numeric_hierarchy.numfield.html">numfield</a></li>
<li><a href="mathcomp.algebra.numeric_hierarchy.orderedzmod.html">orderedzmod</a></li>
<li><a href="mathcomp.algebra.numeric_hierarchy.ssrnum.html">ssrnum</a></li>
</ul>
</details>
</li>
<li><a href="mathcomp.algebra.algebra.html">algebra</a></li>
<li><a href="mathcomp.algebra.all_algebra.html">all_algebra</a></li>
<li><a href="mathcomp.algebra.archimedean.html">archimedean</a></li>
<li><a href="mathcomp.algebra.arithmetic_tactic.html">arithmetic_tactic</a></li>
<li><a href="mathcomp.algebra.binnums.html">binnums</a></li>
<li><a href="mathcomp.algebra.countalg.html">countalg</a></li>
<li><a href="mathcomp.algebra.field_tactic.html">field_tactic</a></li>
<li><a href="mathcomp.algebra.finalg.html">finalg</a></li>
<li><a href="mathcomp.algebra.fraction.html">fraction</a></li>
<li><a href="mathcomp.algebra.intdiv.html">intdiv</a></li>
<li><a href="mathcomp.algebra.interval.html">interval</a></li>
<li><a href="mathcomp.algebra.interval_inference.html">interval_inference</a></li>
<li><a href="mathcomp.algebra.lra.html">lra</a></li>
<li><a href="mathcomp.algebra.matrix.html">matrix</a></li>
<li><a href="mathcomp.algebra.mxalgebra.html">mxalgebra</a></li>
<li><a href="mathcomp.algebra.mxpoly.html">mxpoly</a></li>
<li><a href="mathcomp.algebra.mxred.html">mxred</a></li>
<li><a href="mathcomp.algebra.poly.html">poly</a></li>
<li><a href="mathcomp.algebra.polyXY.html">polyXY</a></li>
<li><a href="mathcomp.algebra.polydiv.html">polydiv</a></li>
<li><a href="mathcomp.algebra.qpoly.html">qpoly</a></li>
<li><a href="mathcomp.algebra.rat.html">rat</a></li>
<li><a href="mathcomp.algebra.ring.html">ring</a></li>
<li><a href="mathcomp.algebra.ring_quotient.html">ring_quotient</a></li>
<li><a href="mathcomp.algebra.ring_tactic.html">ring_tactic</a></li>
<li><a href="mathcomp.algebra.sesquilinear.html">sesquilinear</a></li>
<li><a href="mathcomp.algebra.spectral.html">spectral</a></li>
<li><a href="mathcomp.algebra.ssrint.html">ssrint</a></li>
<li><a href="mathcomp.algebra.tensor.html">tensor</a></li>
<li><a href="mathcomp.algebra.vector.html">vector</a></li>
<li><a href="mathcomp.algebra.zmodp.html">zmodp</a></li>
</ul>
</details>
</li>
<li><details id="mathcomp.all"><summary>all</summary>
<ul>
<li><a href="mathcomp.all.all.html">all</a></li>
</ul>
</details>
</li>
<li><details id="mathcomp.boot"><summary>boot</summary>
<ul>
<li><a href="mathcomp.boot.all_boot.html">all_boot</a></li>
<li><a href="mathcomp.boot.bigop.html">bigop</a></li>
<li><a href="mathcomp.boot.binomial.html">binomial</a></li>
<li><a href="mathcomp.boot.boot.html">boot</a></li>
<li><a href="mathcomp.boot.choice.html">choice</a></li>
<li><a href="mathcomp.boot.div.html">div</a></li>
<li><a href="mathcomp.boot.eqtype.html">eqtype</a></li>
<li><a href="mathcomp.boot.finfun.html">finfun</a></li>
<li><a href="mathcomp.boot.fingraph.html">fingraph</a></li>
<li><a href="mathcomp.boot.finset.html">finset</a></li>
<li><a href="mathcomp.boot.fintype.html">fintype</a></li>
<li><a href="mathcomp.boot.generic_quotient.html">generic_quotient</a></li>
<li><a href="mathcomp.boot.monoid.html">monoid</a></li>
<li><a href="mathcomp.boot.nmodule.html">nmodule</a></li>
<li><a href="mathcomp.boot.path.html">path</a></li>
<li><a href="mathcomp.boot.prime.html">prime</a></li>
<li><a href="mathcomp.boot.seq.html">seq</a></li>
<li><a href="mathcomp.boot.ssrAC.html">ssrAC</a></li>
<li><a href="mathcomp.boot.ssrbool.html">ssrbool</a></li>
<li><a href="mathcomp.boot.ssreflect.html">ssreflect</a></li>
<li><a href="mathcomp.boot.ssrfun.html">ssrfun</a></li>
<li><a href="mathcomp.boot.ssrmatching.html">ssrmatching</a></li>
<li><a href="mathcomp.boot.ssrnat.html">ssrnat</a></li>
<li><a href="mathcomp.boot.ssrnotations.html">ssrnotations</a></li>
<li><a href="mathcomp.boot.tuple.html">tuple</a></li>
</ul>
</details>
</li>
<li><details id="mathcomp.field"><summary>field</summary>
<ul>
<li><a href="mathcomp.field.algC.html">algC</a></li>
<li><a href="mathcomp.field.algebraics_fundamentals.html">algebraics_fundamentals</a></li>
<li><a href="mathcomp.field.algnum.html">algnum</a></li>
<li><a href="mathcomp.field.all_field.html">all_field</a></li>
<li><a href="mathcomp.field.closed_field.html">closed_field</a></li>
<li><a href="mathcomp.field.cyclotomic.html">cyclotomic</a></li>
<li><a href="mathcomp.field.falgebra.html">falgebra</a></li>
<li><a href="mathcomp.field.field.html">field</a></li>
<li><a href="mathcomp.field.fieldext.html">fieldext</a></li>
<li><a href="mathcomp.field.finfield.html">finfield</a></li>
<li><a href="mathcomp.field.galois.html">galois</a></li>
<li><a href="mathcomp.field.qfpoly.html">qfpoly</a></li>
<li><a href="mathcomp.field.separable.html">separable</a></li>
</ul>
</details>
</li>
<li><details id="mathcomp.finite_group"><summary>finite_group</summary>
<ul>
<li><a href="mathcomp.finite_group.action.html">action</a></li>
<li><a href="mathcomp.finite_group.all_fingroup.html">all_fingroup</a></li>
<li><a href="mathcomp.finite_group.automorphism.html">automorphism</a></li>
<li><a href="mathcomp.finite_group.fingroup.html">fingroup</a></li>
<li><a href="mathcomp.finite_group.finite_group.html">finite_group</a></li>
<li><a href="mathcomp.finite_group.gproduct.html">gproduct</a></li>
<li><a href="mathcomp.finite_group.morphism.html">morphism</a></li>
<li><a href="mathcomp.finite_group.perm.html">perm</a></li>
<li><a href="mathcomp.finite_group.presentation.html">presentation</a></li>
<li><a href="mathcomp.finite_group.quotient.html">quotient</a></li>
</ul>
</details>
</li>
<li><details id="mathcomp.group_representation"><summary>group_representation</summary>
<ul>
<li><a href="mathcomp.group_representation.all_character.html">all_character</a></li>
<li><a href="mathcomp.group_representation.character.html">character</a></li>
<li><a href="mathcomp.group_representation.classfun.html">classfun</a></li>
<li><a href="mathcomp.group_representation.group_representation.html">group_representation</a></li>
<li><a href="mathcomp.group_representation.inertia.html">inertia</a></li>
<li><a href="mathcomp.group_representation.integral_char.html">integral_char</a></li>
<li><a href="mathcomp.group_representation.mxabelem.html">mxabelem</a></li>
<li><a href="mathcomp.group_representation.mxrepresentation.html">mxrepresentation</a></li>
<li><a href="mathcomp.group_representation.vcharacter.html">vcharacter</a></li>
</ul>
</details>
</li>
<li><details id="mathcomp.order"><summary>order</summary>
<ul>
<li><a href="mathcomp.order.all_order.html">all_order</a></li>
<li><a href="mathcomp.order.order.html">order</a></li>
<li><a href="mathcomp.order.preorder.html">preorder</a></li>
</ul>
</details>
</li>
<li><details id="mathcomp.solvable"><summary>solvable</summary>
<ul>
<li><a href="mathcomp.solvable.abelian.html">abelian</a></li>
<li><a href="mathcomp.solvable.all_solvable.html">all_solvable</a></li>
<li><a href="mathcomp.solvable.alt.html">alt</a></li>
<li><a href="mathcomp.solvable.burnside_app.html">burnside_app</a></li>
<li><a href="mathcomp.solvable.center.html">center</a></li>
<li><a href="mathcomp.solvable.commutator.html">commutator</a></li>
<li><a href="mathcomp.solvable.cyclic.html">cyclic</a></li>
<li><a href="mathcomp.solvable.extraspecial.html">extraspecial</a></li>
<li><a href="mathcomp.solvable.extremal.html">extremal</a></li>
<li><a href="mathcomp.solvable.finmodule.html">finmodule</a></li>
<li><a href="mathcomp.solvable.frobenius.html">frobenius</a></li>
<li><a href="mathcomp.solvable.gfunctor.html">gfunctor</a></li>
<li><a href="mathcomp.solvable.gseries.html">gseries</a></li>
<li><a href="mathcomp.solvable.hall.html">hall</a></li>
<li><a href="mathcomp.solvable.jordanholder.html">jordanholder</a></li>
<li><a href="mathcomp.solvable.maximal.html">maximal</a></li>
<li><a href="mathcomp.solvable.nilpotent.html">nilpotent</a></li>
<li><a href="mathcomp.solvable.pgroup.html">pgroup</a></li>
<li><a href="mathcomp.solvable.primitive_action.html">primitive_action</a></li>
<li><a href="mathcomp.solvable.solvable.html">solvable</a></li>
<li><a href="mathcomp.solvable.sylow.html">sylow</a></li>
</ul>
</details>
</li>
<li><details id="mathcomp.ssreflect"><summary>ssreflect</summary>
<ul>
<li><a href="mathcomp.ssreflect.all_ssreflect.html">all_ssreflect</a></li>
</ul>
</details>
</li>
</ul>
</details>
</li>
</div>
<div class="coq">
<div class="content">
<p>
<a href="./index.html">Top</a>
</p>
<h1 class="title">Mathematical Components 7cde45af</h1>
<table><tbody>
<tr><td>Files</td>
<td><a href="index_file_A.html">A</a></td><td><a href="index_file_B.html">B</a></td><td><a href="index_file_C.html">C</a></td><td><a href="index_file_D.html">D</a></td><td><a href="index_file_E.html">E</a></td><td><a href="index_file_F.html">F</a></td><td><a href="index_file_G.html">G</a></td><td><a href="index_file_H.html">H</a></td><td><a href="index_file_I.html">I</a></td><td><a href="index_file_J.html">J</a></td><td>K</td><td><a href="index_file_L.html">L</a></td><td><a href="index_file_M.html">M</a></td><td><a href="index_file_N.html">N</a></td><td><a href="index_file_O.html">O</a></td><td><a href="index_file_P.html">P</a></td><td><a href="index_file_Q.html">Q</a></td><td><a href="index_file_R.html">R</a></td><td><a href="index_file_S.html">S</a></td><td><a href="index_file_T.html">T</a></td><td>U</td><td><a href="index_file_V.html">V</a></td><td>W</td><td>X</td><td>Y</td><td><a href="index_file_Z.html">Z</a></td><td>_</td></tr>
<tr><td>Definitions</td>
<td><a href="index_def_A.html">A</a></td><td><a href="index_def_B.html">B</a></td><td><a href="index_def_C.html">C</a></td><td><a href="index_def_D.html">D</a></td><td><a href="index_def_E.html">E</a></td><td><a href="index_def_F.html">F</a></td><td><a href="index_def_G.html">G</a></td><td><a href="index_def_H.html">H</a></td><td><a href="index_def_I.html">I</a></td><td><a href="index_def_J.html">J</a></td><td><a href="index_def_K.html">K</a></td><td><a href="index_def_L.html">L</a></td><td><a href="index_def_M.html">M</a></td><td><a href="index_def_N.html">N</a></td><td><a href="index_def_O.html">O</a></td><td><a href="index_def_P.html">P</a></td><td><a href="index_def_Q.html">Q</a></td><td><a href="index_def_R.html">R</a></td><td><a href="index_def_S.html">S</a></td><td><a href="index_def_T.html">T</a></td><td><a href="index_def_U.html">U</a></td><td><a href="index_def_V.html">V</a></td><td><a href="index_def_W.html">W</a></td><td><a href="index_def_X.html">X</a></td><td>Y</td><td><a href="index_def_Z.html">Z</a></td><td>_</td></tr>
<tr><td>Lemmas</td>
<td><a href="index_prf_A.html">A</a></td><td><a href="index_prf_B.html">B</a></td><td><a href="index_prf_C.html">C</a></td><td><a href="index_prf_D.html">D</a></td><td><a href="index_prf_E.html">E</a></td><td><a href="index_prf_F.html">F</a></td><td><a href="index_prf_G.html">G</a></td><td><a href="index_prf_H.html">H</a></td><td><a href="index_prf_I.html">I</a></td><td><a href="index_prf_J.html">J</a></td><td><a href="index_prf_K.html">K</a></td><td><a href="index_prf_L.html">L</a></td><td><a href="index_prf_M.html">M</a></td><td><a href="index_prf_N.html">N</a></td><td><a href="index_prf_O.html">O</a></td><td><a href="index_prf_P.html">P</a></td><td><a href="index_prf_Q.html">Q</a></td><td><a href="index_prf_R.html">R</a></td><td><a href="index_prf_S.html">S</a></td><td><a href="index_prf_T.html">T</a></td><td><a href="index_prf_U.html">U</a></td><td><a href="index_prf_V.html">V</a></td><td><a href="index_prf_W.html">W</a></td><td><a href="index_prf_X.html">X</a></td><td>Y</td><td><a href="index_prf_Z.html">Z</a></td><td>_</td></tr>
<tr><td>Abbreviations</td>
<td><a href="index_abbrev_A.html">A</a></td><td><a href="index_abbrev_B.html">B</a></td><td><a href="index_abbrev_C.html">C</a></td><td><a href="index_abbrev_D.html">D</a></td><td><a href="index_abbrev_E.html">E</a></td><td><a href="index_abbrev_F.html">F</a></td><td><a href="index_abbrev_G.html">G</a></td><td><a href="index_abbrev_H.html">H</a></td><td><a href="index_abbrev_I.html">I</a></td><td><a href="index_abbrev_J.html">J</a></td><td><a href="index_abbrev_K.html">K</a></td><td><a href="index_abbrev_L.html">L</a></td><td><a href="index_abbrev_M.html">M</a></td><td><a href="index_abbrev_N.html">N</a></td><td><a href="index_abbrev_O.html">O</a></td><td><a href="index_abbrev_P.html">P</a></td><td><a href="index_abbrev_Q.html">Q</a></td><td><a href="index_abbrev_R.html">R</a></td><td><a href="index_abbrev_S.html">S</a></td><td><a href="index_abbrev_T.html">T</a></td><td><a href="index_abbrev_U.html">U</a></td><td><a href="index_abbrev_V.html">V</a></td><td><a href="index_abbrev_W.html">W</a></td><td><a href="index_abbrev_X.html">X</a></td><td>Y</td><td><a href="index_abbrev_Z.html">Z</a></td><td>_</td></tr>
<tr><td>Global Index</td>
<td><a href="index_global_A.html">A</a></td><td><a href="index_global_B.html">B</a></td><td><a href="index_global_C.html">C</a></td><td><a href="index_global_D.html">D</a></td><td><a href="index_global_E.html">E</a></td><td><a href="index_global_F.html">F</a></td><td><a href="index_global_G.html">G</a></td><td><a href="index_global_H.html">H</a></td><td><a href="index_global_I.html">I</a></td><td><a href="index_global_J.html">J</a></td><td><a href="index_global_K.html">K</a></td><td><a href="index_global_L.html">L</a></td><td><a href="index_global_M.html">M</a></td><td><a href="index_global_N.html">N</a></td><td><a href="index_global_O.html">O</a></td><td><a href="index_global_P.html">P</a></td><td><a href="index_global_Q.html">Q</a></td><td><a href="index_global_R.html">R</a></td><td><a href="index_global_S.html">S</a></td><td><a href="index_global_T.html">T</a></td><td><a href="index_global_U.html">U</a></td><td><a href="index_global_V.html">V</a></td><td><a href="index_global_W.html">W</a></td><td><a href="index_global_X.html">X</a></td><td>Y</td><td><a href="index_global_Z.html">Z</a></td><td>_</td></tr>
<tr><td><a href="index_notations.html">Notations</a></td></tr></tbody></table><h2>Mathematical Structures (Mathematical Components 7cde45af only)</h2><img src="hierarchy_graph.png" title usemap="#Hierarchy" class="img-darkmode-enable"/>
<map id="Hierarchy" name="Hierarchy">
<area shape="poly" id="node3" href="mathcomp.finite_group.fingroup.html#FinGroup" title="FinGroup" alt="" coords="1236,797,1233,790,1224,783,1210,778,1193,775,1173,773,1154,775,1137,778,1123,783,1114,790,1111,797,1114,805,1123,811,1137,817,1154,820,1173,821,1193,820,1210,817,1224,811,1233,805"/>
<area shape="poly" id="node4" href="mathcomp.finite_group.fingroup.html#FinStarMonoid" title="FinStarMonoid" alt="" coords="1372,701,1367,694,1354,687,1334,682,1309,679,1281,677,1253,679,1228,682,1208,687,1195,694,1191,701,1195,709,1208,715,1228,721,1253,724,1281,725,1309,724,1334,721,1354,715,1367,709"/>
<area shape="poly" id="node5" href="mathcomp.field.galois.html#SplittingField" title="SplittingField" alt="" coords="7743,29,7739,22,7728,15,7710,10,7687,7,7661,5,7636,7,7613,10,7595,15,7583,22,7579,29,7583,37,7595,43,7613,49,7636,52,7661,53,7687,52,7710,49,7728,43,7739,37"/>
<area shape="poly" id="node6" href="mathcomp.field.fieldext.html#FieldExt" title="FieldExt" alt="" coords="8326,1277,8323,1270,8315,1263,8303,1258,8287,1255,8269,1253,8252,1255,8236,1258,8223,1263,8215,1270,8212,1277,8215,1285,8223,1291,8236,1297,8252,1300,8269,1301,8287,1300,8303,1297,8315,1291,8323,1285"/>
<area shape="poly" id="node8" href="mathcomp.field.falgebra.html#Falgebra" title="Falgebra" alt="" coords="8648,1181,8645,1174,8637,1167,8625,1162,8608,1159,8591,1157,8573,1159,8557,1162,8544,1167,8536,1174,8533,1181,8536,1189,8544,1195,8557,1201,8573,1204,8591,1205,8608,1204,8625,1201,8637,1195,8645,1189"/>
<area shape="poly" id="node9" href="mathcomp.boot.monoid.html#SubGroup" title="SubGroup" alt="" coords="1086,797,1083,790,1074,783,1060,778,1041,775,1021,773,1001,775,983,778,969,783,959,790,956,797,959,805,969,811,983,817,1001,820,1021,821,1041,820,1060,817,1074,811,1083,805"/>
<area shape="poly" id="node10" href="mathcomp.boot.monoid.html#SubMonoid" title="SubMonoid" alt="" coords="1164,605,1160,598,1150,591,1134,586,1113,583,1091,581,1068,583,1048,586,1031,591,1021,598,1017,605,1021,613,1031,619,1048,625,1068,628,1091,629,1113,628,1134,625,1150,619,1160,613"/>
<area shape="poly" id="node11" href="mathcomp.boot.monoid.html#SubUMagma" title="SubUMagma" alt="" coords="1152,509,1148,502,1137,495,1119,490,1096,487,1071,485,1046,487,1023,490,1005,495,993,502,989,509,993,517,1005,523,1023,529,1046,532,1071,533,1096,532,1119,529,1137,523,1148,517"/>
<area shape="poly" id="node12" href="mathcomp.boot.monoid.html#SubBaseUMagma" title="SubBaseUMagma" alt="" coords="1315,413,1310,406,1295,399,1271,394,1242,391,1209,389,1177,391,1147,394,1124,399,1109,406,1104,413,1109,421,1124,427,1147,433,1177,436,1209,437,1242,436,1271,433,1295,427,1310,421"/>
<area shape="poly" id="node13" href="mathcomp.boot.monoid.html#SubSemigroup" title="SubSemigroup" alt="" coords="1515,413,1511,406,1498,399,1479,394,1454,391,1427,389,1399,391,1375,394,1355,399,1343,406,1338,413,1343,421,1355,427,1375,433,1399,436,1427,437,1454,436,1479,433,1498,427,1511,421"/>
<area shape="poly" id="node14" href="mathcomp.boot.monoid.html#SubMagma" title="SubMagma" alt="" coords="1459,317,1456,310,1445,303,1429,298,1409,295,1387,293,1364,295,1344,298,1328,303,1318,310,1314,317,1318,325,1328,331,1344,337,1364,340,1387,341,1409,340,1429,337,1445,331,1456,325"/>
<area shape="poly" id="node15" href="mathcomp.boot.monoid.html#GroupClosed" title="GroupClosed" alt="" coords="8248,221,8244,214,8233,207,8215,202,8193,199,8168,197,8143,199,8121,202,8103,207,8092,214,8088,221,8092,229,8103,235,8121,241,8143,244,8168,245,8193,244,8215,241,8233,235,8244,229"/>
<area shape="poly" id="node16" href="mathcomp.boot.monoid.html#InvClosed" title="InvClosed" alt="" coords="8140,125,8137,118,8127,111,8113,106,8095,103,8075,101,8055,103,8036,106,8022,111,8013,118,8010,125,8013,133,8022,139,8036,145,8055,148,8075,149,8095,148,8113,145,8127,139,8137,133"/>
<area shape="poly" id="node17" href="mathcomp.boot.monoid.html#UMagmaClosed" title="UMagmaClosed" alt="" coords="8356,125,8352,118,8338,111,8317,106,8290,103,8260,101,8230,103,8203,106,8182,111,8168,118,8164,125,8168,133,8182,139,8203,145,8230,148,8260,149,8290,148,8317,145,8338,139,8352,133"/>
<area shape="poly" id="node18" href="mathcomp.boot.monoid.html#MulClosed" title="MulClosed" alt="" coords="8330,29,8326,22,8317,15,8301,10,8282,7,8260,5,8238,7,8219,10,8204,15,8194,22,8190,29,8194,37,8204,43,8219,49,8238,52,8260,53,8282,52,8301,49,8317,43,8326,37"/>
<area shape="poly" id="node19" href="mathcomp.boot.monoid.html#UMagmaMorphism" title="UMagmaMorphism" alt="" coords="8610,125,8604,118,8588,111,8562,106,8530,103,8495,101,8459,103,8427,106,8402,111,8385,118,8380,125,8385,133,8402,139,8427,145,8459,148,8495,149,8530,148,8562,145,8588,139,8604,133"/>
<area shape="poly" id="node20" href="mathcomp.boot.monoid.html#Multiplicative" title="Multiplicative" alt="" coords="8580,29,8575,22,8563,15,8545,10,8521,7,8495,5,8468,7,8445,10,8426,15,8414,22,8410,29,8414,37,8426,43,8445,49,8468,52,8495,53,8521,52,8545,49,8563,43,8575,37"/>
<area shape="poly" id="node21" href="mathcomp.boot.monoid.html#Group" title="Group" alt="" coords="1167,701,1165,694,1159,687,1148,682,1136,679,1121,677,1107,679,1094,682,1084,687,1078,694,1075,701,1078,709,1084,715,1094,721,1107,724,1121,725,1136,724,1148,721,1159,715,1165,709"/>
<area shape="poly" id="node22" href="mathcomp.boot.monoid.html#StarMonoid" title="StarMonoid" alt="" coords="1355,605,1352,598,1341,591,1325,586,1304,583,1281,581,1259,583,1238,586,1222,591,1211,598,1207,605,1211,613,1222,619,1238,625,1259,628,1281,629,1304,628,1325,625,1341,619,1352,613"/>
<area shape="poly" id="node23" href="mathcomp.boot.monoid.html#BaseGroup" title="BaseGroup" alt="" coords="1785,317,1781,310,1771,303,1756,298,1736,295,1715,293,1693,295,1674,298,1658,303,1648,310,1645,317,1648,325,1658,331,1674,337,1693,340,1715,341,1736,340,1756,337,1771,331,1781,325"/>
<area shape="poly" id="node24" href="mathcomp.boot.monoid.html#Monoid" title="Monoid" alt="" coords="1335,509,1333,502,1325,495,1313,490,1298,487,1281,485,1265,487,1250,490,1238,495,1230,502,1227,509,1230,517,1238,523,1250,529,1265,532,1281,533,1298,532,1313,529,1325,523,1333,517"/>
<area shape="poly" id="node25" href="mathcomp.boot.monoid.html#UMagma" title="UMagma" alt="" coords="1080,413,1077,406,1068,399,1054,394,1037,391,1017,389,998,391,981,394,967,399,958,406,955,413,958,421,967,427,981,433,998,436,1017,437,1037,436,1054,433,1068,427,1077,421"/>
<area shape="poly" id="node26" href="mathcomp.boot.monoid.html#ChoiceBaseUMagma" title="ChoiceBaseUMagma" alt="" coords="1290,317,1284,310,1267,303,1240,298,1207,295,1169,293,1132,295,1098,298,1071,303,1054,310,1048,317,1054,325,1071,331,1098,337,1132,340,1169,341,1207,340,1240,337,1267,331,1284,325"/>
<area shape="poly" id="node27" href="mathcomp.boot.monoid.html#BaseUMagma" title="BaseUMagma" alt="" coords="1357,221,1353,214,1340,207,1321,202,1297,199,1271,197,1244,199,1220,202,1201,207,1189,214,1184,221,1189,229,1201,235,1220,241,1244,244,1271,245,1297,244,1321,241,1340,235,1353,229"/>
<area shape="poly" id="node28" href="mathcomp.boot.monoid.html#Semigroup" title="Semigroup" alt="" coords="1621,317,1618,310,1608,303,1593,298,1573,295,1552,293,1531,295,1511,298,1496,303,1486,310,1483,317,1486,325,1496,331,1511,337,1531,340,1552,341,1573,340,1593,337,1608,331,1618,325"/>
<area shape="poly" id="node29" href="mathcomp.boot.monoid.html#ChoiceMagma" title="ChoiceMagma" alt="" coords="1558,221,1553,214,1541,207,1521,202,1497,199,1469,197,1442,199,1417,202,1398,207,1385,214,1381,221,1385,229,1398,235,1417,241,1442,244,1469,245,1497,244,1521,241,1541,235,1553,229"/>
<area shape="poly" id="node30" href="mathcomp.boot.monoid.html#Magma" title="Magma" alt="" coords="1428,125,1426,118,1418,111,1406,106,1391,103,1375,101,1358,103,1343,106,1331,111,1324,118,1321,125,1324,133,1331,139,1343,145,1358,148,1375,149,1391,148,1406,145,1418,139,1426,133"/>
<area shape="poly" id="node31" href="mathcomp.boot.generic_quotient.html#EqQuotient" title="EqQuotient" alt="" coords="7327,125,7324,118,7314,111,7298,106,7278,103,7256,101,7234,103,7214,106,7198,111,7188,118,7185,125,7188,133,7198,139,7214,145,7234,148,7256,149,7278,148,7298,145,7314,139,7324,133"/>
<area shape="poly" id="node32" href="mathcomp.algebra.ring_quotient.html#ZmodQuotient" title="ZmodQuotient" alt="" coords="8317,701,8313,694,8300,687,8281,682,8256,679,8229,677,8202,679,8178,682,8159,687,8146,694,8142,701,8146,709,8159,715,8178,721,8202,724,8229,725,8256,724,8281,721,8300,715,8313,709"/>
<area shape="poly" id="node59" href="mathcomp.algebra.ring_quotient.html#NzRingQuotient" title="NzRingQuotient" alt="" coords="8514,893,8510,886,8496,879,8475,874,8448,871,8419,869,8389,871,8362,874,8341,879,8328,886,8323,893,8328,901,8341,907,8362,913,8389,916,8419,917,8448,916,8475,913,8496,907,8510,901"/>
<area shape="poly" id="node33" href="mathcomp.boot.generic_quotient.html#Quotient" title="Quotient" alt="" coords="8719,29,8716,22,8708,15,8695,10,8679,7,8661,5,8644,7,8628,10,8615,15,8607,22,8604,29,8607,37,8615,43,8628,49,8644,52,8661,53,8679,52,8695,49,8708,43,8716,37"/>
<area shape="poly" id="node34" href="mathcomp.boot.fintype.html#SubFinite" title="SubFinite" alt="" coords="4900,509,4897,502,4888,495,4874,490,4857,487,4837,485,4818,487,4801,490,4787,495,4778,502,4775,509,4778,517,4787,523,4801,529,4818,532,4837,533,4857,532,4874,529,4888,523,4897,517"/>
<area shape="poly" id="node35" href="mathcomp.boot.fintype.html#Finite" title="Finite" alt="" coords="8830,29,8828,22,8822,15,8812,10,8800,7,8787,5,8773,7,8761,10,8752,15,8746,22,8743,29,8746,37,8752,43,8761,49,8773,52,8787,53,8800,52,8812,49,8822,43,8828,37"/>
<area shape="poly" id="node36" href="mathcomp.boot.eqtype.html#SubEquality" title="SubEquality" alt="" coords="4705,125,4701,118,4690,111,4674,106,4653,103,4629,101,4606,103,4585,106,4568,111,4558,118,4554,125,4558,133,4568,139,4585,145,4606,148,4629,149,4653,148,4674,145,4690,139,4701,133"/>
<area shape="poly" id="node37" href="mathcomp.boot.choice.html#SubChoice" title="SubChoice" alt="" coords="4698,221,4694,214,4685,207,4670,202,4651,199,4629,197,4608,199,4589,202,4574,207,4564,214,4561,221,4564,229,4574,235,4589,241,4608,244,4629,245,4651,244,4670,241,4685,235,4694,229"/>
<area shape="poly" id="node40" href="mathcomp.boot.choice.html#SubCountable" title="SubCountable" alt="" coords="4922,413,4917,406,4905,399,4887,394,4863,391,4837,389,4811,391,4788,394,4769,399,4757,406,4753,413,4757,421,4769,427,4788,433,4811,436,4837,437,4863,436,4887,433,4905,427,4917,421"/>
<area shape="poly" id="node38" href="mathcomp.boot.eqtype.html#SubType" title="SubType" alt="" coords="4688,29,4685,22,4677,15,4664,10,4648,7,4629,5,4611,7,4595,10,4582,15,4573,22,4570,29,4573,37,4582,43,4595,49,4611,52,4629,53,4648,52,4664,49,4677,43,4685,37"/>
<area shape="poly" id="node39" href="mathcomp.boot.eqtype.html#Equality" title="Equality" alt="" coords="8967,29,8964,22,8956,15,8944,10,8928,7,8911,5,8893,7,8878,10,8865,15,8857,22,8855,29,8857,37,8865,43,8878,49,8893,52,8911,53,8928,52,8944,49,8956,43,8964,37"/>
<area shape="poly" id="node41" href="mathcomp.boot.choice.html#Countable" title="Countable" alt="" coords="4902,317,4899,310,4890,303,4876,298,4857,295,4837,293,4817,295,4799,298,4785,303,4775,310,4772,317,4775,325,4785,331,4799,337,4817,340,4837,341,4857,340,4876,337,4890,331,4899,325"/>
<area shape="poly" id="node46" href="mathcomp.boot.choice.html#Choice" title="Choice" alt="" coords="9089,29,9087,22,9080,15,9069,10,9055,7,9040,5,9025,7,9011,10,9000,15,8993,22,8991,29,8993,37,9000,43,9011,49,9025,52,9040,53,9055,52,9069,49,9080,43,9087,37"/>
<area shape="poly" id="node47" href="mathcomp.algebra.vector.html#NzVector" title="NzVector" alt="" coords="10718,893,10715,886,10707,879,10693,874,10676,871,10657,869,10639,871,10622,874,10608,879,10599,886,10596,893,10599,901,10608,907,10622,913,10639,916,10657,917,10676,916,10693,913,10707,907,10715,901"/>
<area shape="poly" id="node48" href="mathcomp.algebra.vector.html#NzSemiVector" title="NzSemiVector" alt="" coords="10712,797,10708,790,10696,783,10676,778,10652,775,10625,773,10599,775,10574,778,10555,783,10543,790,10538,797,10543,805,10555,811,10574,817,10599,820,10625,821,10652,820,10676,817,10696,811,10708,805"/>
<area shape="poly" id="node49" href="mathcomp.algebra.vector.html#Vector" title="Vector" alt="" coords="9207,29,9204,22,9198,15,9187,10,9174,7,9160,5,9146,7,9133,10,9122,15,9116,22,9113,29,9116,37,9122,43,9133,49,9146,52,9160,53,9174,52,9187,49,9198,43,9204,37"/>
<area shape="poly" id="node50" href="mathcomp.algebra.vector.html#SemiVector" title="SemiVector" alt="" coords="9375,29,9372,22,9361,15,9345,10,9325,7,9303,5,9280,7,9260,10,9244,15,9234,22,9230,29,9234,37,9244,43,9260,49,9280,52,9303,53,9325,52,9345,49,9361,43,9372,37"/>
<area shape="poly" id="node51" href="mathcomp.algebra.sesquilinear.html#Dot" title="Dot" alt="" coords="9555,221,9553,214,9548,207,9540,202,9530,199,9519,197,9508,199,9498,202,9490,207,9484,214,9483,221,9484,229,9490,235,9498,241,9508,244,9519,245,9530,244,9540,241,9548,235,9553,229"/>
<area shape="poly" id="node52" href="mathcomp.algebra.sesquilinear.html#Hermitian" title="Hermitian" alt="" coords="9584,125,9581,118,9571,111,9557,106,9539,103,9519,101,9499,103,9480,106,9466,111,9457,118,9454,125,9457,133,9466,139,9480,145,9499,148,9519,149,9539,148,9557,145,9571,139,9581,133"/>
<area shape="poly" id="node53" href="mathcomp.algebra.sesquilinear.html#Bilinear" title="Bilinear" alt="" coords="9790,29,9788,22,9780,15,9768,10,9753,7,9736,5,9719,7,9704,10,9692,15,9685,22,9682,29,9685,37,9692,43,9704,49,9719,52,9736,53,9753,52,9768,49,9780,43,9788,37"/>
<area shape="poly" id="node54" href="mathcomp.algebra.sesquilinear.html#InvolutiveRMorphism" title="InvolutiveRMorphism" alt="" coords="9830,221,9824,214,9806,207,9778,202,9743,199,9704,197,9665,199,9630,202,9602,207,9584,214,9578,221,9584,229,9602,235,9630,241,9665,244,9704,245,9743,244,9778,241,9806,235,9824,229"/>
<area shape="poly" id="node55" href="mathcomp.algebra.ring_quotient.html#PrimeIdealr" title="PrimeIdealr" alt="" coords="11435,413,11431,406,11421,399,11404,394,11384,391,11361,389,11339,391,11318,394,11302,399,11292,406,11288,413,11292,421,11302,427,11318,433,11339,436,11361,437,11384,436,11404,433,11421,427,11431,421"/>
<area shape="poly" id="node56" href="mathcomp.algebra.ring_quotient.html#Idealr" title="Idealr" alt="" coords="11405,317,11402,310,11396,303,11387,298,11375,295,11361,293,11348,295,11336,298,11326,303,11320,310,11318,317,11320,325,11326,331,11336,337,11348,340,11361,341,11375,340,11387,337,11396,331,11402,325"/>
<area shape="poly" id="node57" href="mathcomp.algebra.ring_quotient.html#ProperIdeal" title="ProperIdeal" alt="" coords="11544,221,11540,214,11530,207,11514,202,11494,199,11472,197,11450,199,11430,202,11414,207,11404,214,11400,221,11404,229,11414,235,11430,241,11450,244,11472,245,11494,244,11514,241,11530,235,11540,229"/>
<area shape="poly" id="node58" href="mathcomp.algebra.ring_quotient.html#UnitRingQuotient" title="UnitRingQuotient" alt="" coords="7779,989,7774,982,7760,975,7737,970,7708,967,7676,965,7644,967,7615,970,7592,975,7578,982,7573,989,7578,997,7592,1003,7615,1009,7644,1012,7676,1013,7708,1012,7737,1009,7760,1003,7774,997"/>
</map>
<h2>Clickable Dependency Graph of Files</h2><img src="dependency_graph.png" usemap="#depend" class="img-darkmode-enable"/><map id="depend" name="depend">
<area shape="rect" id="node1" href="mathcomp.algebra.numeric_hierarchy.orderedzmod.html" title="orderedzmod" alt="" coords="2132,1823,2281,1871"/>
<area shape="rect" id="node2" href="mathcomp.algebra.numeric_hierarchy.numdomain.html" title="numdomain" alt="" coords="2143,1919,2281,1967"/>
<area shape="rect" id="node3" href="mathcomp.algebra.numeric_hierarchy.numfield.html" title="numfield" alt="" coords="2157,2021,2267,2069"/>
<area shape="rect" id="node4" href="mathcomp.algebra.numeric_hierarchy.ssrnum.html" title="ssrnum" alt="" coords="2191,2117,2281,2165"/>
<area shape="rect" id="node34" href="mathcomp.algebra.ssrint.html" title="ssrint" alt="" coords="2022,2117,2095,2165"/>
<area shape="rect" id="node37" href="mathcomp.algebra.sesquilinear.html" title="sesquilinear" alt="" coords="1865,2326,2002,2374"/>
<area shape="rect" id="node12" href="mathcomp.algebra.binnums.html" title="binnums" alt="" coords="1902,2422,2007,2470"/>
<area shape="rect" id="node39" href="mathcomp.algebra.tensor.html" title="tensor" alt="" coords="1726,2422,1807,2470"/>
<area shape="rect" id="node51" href="mathcomp.field.algebraics_fundamentals.html" title="algebraics_fundamentals" alt="" coords="3911,2614,4174,2662"/>
<area shape="rect" id="node5" href="mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras.html" title="rings_modules_and_algebras" alt="" coords="1890,1406,2193,1454"/>
<area shape="rect" id="node6" href="mathcomp.algebra.algebraic_hierarchy.divalg.html" title="divalg" alt="" coords="2083,1502,2165,1550"/>
<area shape="rect" id="node7" href="mathcomp.algebra.algebraic_hierarchy.decfield.html" title="decfield" alt="" coords="2046,1615,2146,1663"/>
<area shape="rect" id="node15" href="mathcomp.algebra.fraction.html" title="fraction" alt="" coords="2242,1615,2339,1663"/>
<area shape="rect" id="node33" href="mathcomp.algebra.ring_quotient.html" title="ring_quotient" alt="" coords="2549,1615,2702,1663"/>
<area shape="rect" id="node8" href="mathcomp.algebra.algebraic_hierarchy.ssralg.html" title="ssralg" alt="" coords="2087,1711,2164,1759"/>
<area shape="rect" id="node13" href="mathcomp.algebra.countalg.html" title="countalg" alt="" coords="1762,1711,1867,1759"/>
<area shape="rect" id="node18" href="mathcomp.algebra.interval_inference.html" title="interval_inference" alt="" coords="1534,2230,1733,2278"/>
<area shape="rect" id="node55" href="mathcomp.field.closed_field.html" title="closed_field" alt="" coords="4034,2518,4174,2566"/>
<area shape="rect" id="node57" href="mathcomp.field.falgebra.html" title="falgebra" alt="" coords="3849,2230,3951,2278"/>
<area shape="rect" id="node80" href="mathcomp.solvable.cyclic.html" title="cyclic" alt="" coords="3313,2021,3394,2069"/>
<area shape="rect" id="node9" href="mathcomp.algebra.algebra.html" title="algebra" alt="" coords="2105,2716,2199,2764"/>
<area shape="rect" id="node10" href="mathcomp.algebra.all_algebra.html" title="all_algebra" alt="" coords="2087,2812,2217,2860"/>
<area shape="rect" id="node40" href="mathcomp.all.all.html" title="all" alt="" coords="4800,3202,4872,3250"/>
<area shape="rect" id="node11" href="mathcomp.algebra.archimedean.html" title="archimedean" alt="" coords="2027,2230,2173,2278"/>
<area shape="rect" id="node29" href="mathcomp.algebra.rat.html" title="rat" alt="" coords="2197,2326,2269,2374"/>
<area shape="rect" id="node30" href="mathcomp.algebra.ring_tactic.html" title="ring_tactic" alt="" coords="1892,2518,2018,2566"/>
<area shape="rect" id="node14" href="mathcomp.algebra.finalg.html" title="finalg" alt="" coords="2377,1823,2455,1871"/>
<area shape="rect" id="node26" href="mathcomp.algebra.poly.html" title="poly" alt="" coords="2744,1823,2816,1871"/>
<area shape="rect" id="node36" href="mathcomp.algebra.zmodp.html" title="zmodp" alt="" coords="2719,1919,2806,1967"/>
<area shape="rect" id="node16" href="mathcomp.algebra.intdiv.html" title="intdiv" alt="" coords="2368,2230,2446,2278"/>
<area shape="rect" id="node17" href="mathcomp.algebra.interval.html" title="interval" alt="" coords="2552,1823,2648,1871"/>
<area shape="rect" id="node19" href="mathcomp.algebra.arithmetic_tactic.html" title="arithmetic_tactic" alt="" coords="1336,2614,1523,2662"/>
<area shape="rect" id="node20" href="mathcomp.algebra.lra.html" title="lra" alt="" coords="1393,2716,1465,2764"/>
<area shape="rect" id="node21" href="mathcomp.algebra.matrix.html" title="matrix" alt="" coords="2720,2021,2805,2069"/>
<area shape="rect" id="node22" href="mathcomp.algebra.mxalgebra.html" title="mxalgebra" alt="" coords="2691,2117,2816,2165"/>
<area shape="rect" id="node82" href="mathcomp.solvable.extremal.html" title="extremal" alt="" coords="3533,2716,3640,2764"/>
<area shape="rect" id="node23" href="mathcomp.algebra.mxpoly.html" title="mxpoly" alt="" coords="2720,2230,2816,2278"/>
<area shape="rect" id="node35" href="mathcomp.algebra.vector.html" title="vector" alt="" coords="2542,2230,2624,2278"/>
<area shape="rect" id="node24" href="mathcomp.algebra.mxred.html" title="mxred" alt="" coords="2365,2326,2448,2374"/>
<area shape="rect" id="node27" href="mathcomp.algebra.polyXY.html" title="polyXY" alt="" coords="2718,2326,2816,2374"/>
<area shape="rect" id="node28" href="mathcomp.algebra.qpoly.html" title="qpoly" alt="" coords="2544,2326,2621,2374"/>
<area shape="rect" id="node48" href="mathcomp.group_representation.mxrepresentation.html" title="mxrepresentation" alt="" coords="4220,2716,4410,2764"/>
<area shape="rect" id="node58" href="mathcomp.field.fieldext.html" title="fieldext" alt="" coords="3924,2326,4020,2374"/>
<area shape="rect" id="node38" href="mathcomp.algebra.spectral.html" title="spectral" alt="" coords="2103,2422,2201,2470"/>
<area shape="rect" id="node25" href="mathcomp.algebra.polydiv.html" title="polydiv" alt="" coords="2500,2117,2596,2165"/>
<area shape="rect" id="node62" href="mathcomp.field.separable.html" title="separable" alt="" coords="3859,2422,3973,2470"/>
<area shape="rect" id="node61" href="mathcomp.field.qfpoly.html" title="qfpoly" alt="" coords="4039,3004,4124,3052"/>
<area shape="rect" id="node31" href="mathcomp.algebra.field_tactic.html" title="field_tactic" alt="" coords="2396,2614,2529,2662"/>
<area shape="rect" id="node32" href="mathcomp.algebra.ring.html" title="ring" alt="" coords="2427,2716,2499,2764"/>
<area shape="rect" id="node41" href="mathcomp.group_representation.group_representation.html" title="group_representation" alt="" coords="4313,3100,4540,3148"/>
<area shape="rect" id="node42" href="mathcomp.group_representation.all_character.html" title="all_character" alt="" coords="4352,3202,4501,3250"/>
<area shape="rect" id="node43" href="mathcomp.group_representation.character.html" title="character" alt="" coords="4487,2812,4598,2860"/>
<area shape="rect" id="node45" href="mathcomp.group_representation.inertia.html" title="inertia" alt="" coords="4220,2908,4305,2956"/>
<area shape="rect" id="node46" href="mathcomp.group_representation.integral_char.html" title="integral_char" alt="" coords="4401,2908,4551,2956"/>
<area shape="rect" id="node44" href="mathcomp.group_representation.classfun.html" title="classfun" alt="" coords="4506,2716,4606,2764"/>
<area shape="rect" id="node49" href="mathcomp.group_representation.vcharacter.html" title="vcharacter" alt="" coords="4318,3004,4442,3052"/>
<area shape="rect" id="node47" href="mathcomp.group_representation.mxabelem.html" title="mxabelem" alt="" coords="4538,3004,4662,3052"/>
<area shape="rect" id="node50" href="mathcomp.field.algC.html" title="algC" alt="" coords="4003,2716,4075,2764"/>
<area shape="rect" id="node56" href="mathcomp.field.cyclotomic.html" title="cyclotomic" alt="" coords="3970,2812,4100,2860"/>
<area shape="rect" id="node52" href="mathcomp.field.algnum.html" title="algnum" alt="" coords="3849,3004,3943,3052"/>
<area shape="rect" id="node53" href="mathcomp.field.field.html" title="field" alt="" coords="4045,3100,4117,3148"/>
<area shape="rect" id="node54" href="mathcomp.field.all_field.html" title="all_field" alt="" coords="4030,3202,4133,3250"/>
<area shape="rect" id="node59" href="mathcomp.field.finfield.html" title="finfield" alt="" coords="4031,2908,4124,2956"/>
<area shape="rect" id="node60" href="mathcomp.field.galois.html" title="galois" alt="" coords="3859,2518,3938,2566"/>
<area shape="rect" id="node63" href="mathcomp.finite_group.action.html" title="action" alt="" coords="1047,1823,1129,1871"/>
<area shape="rect" id="node68" href="mathcomp.finite_group.gproduct.html" title="gproduct" alt="" coords="1034,1919,1142,1967"/>
<area shape="rect" id="node64" href="mathcomp.finite_group.finite_group.html" title="finite_group" alt="" coords="1000,2021,1141,2069"/>
<area shape="rect" id="node65" href="mathcomp.finite_group.all_fingroup.html" title="all_fingroup" alt="" coords="1000,2117,1141,2165"/>
<area shape="rect" id="node66" href="mathcomp.finite_group.automorphism.html" title="automorphism" alt="" coords="807,1615,969,1663"/>
<area shape="rect" id="node72" href="mathcomp.finite_group.quotient.html" title="quotient" alt="" coords="1036,1711,1137,1759"/>
<area shape="rect" id="node67" href="mathcomp.finite_group.fingroup.html" title="fingroup" alt="" coords="870,1261,975,1309"/>
<area shape="rect" id="node69" href="mathcomp.finite_group.morphism.html" title="morphism" alt="" coords="868,1406,988,1454"/>
<area shape="rect" id="node85" href="mathcomp.solvable.gfunctor.html" title="gfunctor" alt="" coords="3074,2021,3177,2069"/>
<area shape="rect" id="node70" href="mathcomp.finite_group.perm.html" title="perm" alt="" coords="829,1502,901,1550"/>
<area shape="rect" id="node71" href="mathcomp.finite_group.presentation.html" title="presentation" alt="" coords="1064,1615,1205,1663"/>
<area shape="rect" id="node73" href="mathcomp.solvable.abelian.html" title="abelian" alt="" coords="3374,2518,3466,2566"/>
<area shape="rect" id="node89" href="mathcomp.solvable.maximal.html" title="maximal" alt="" coords="3357,2614,3464,2662"/>
<area shape="rect" id="node74" href="mathcomp.solvable.solvable.html" title="solvable" alt="" coords="3185,2908,3287,2956"/>
<area shape="rect" id="node75" href="mathcomp.solvable.all_solvable.html" title="all_solvable" alt="" coords="3166,3004,3306,3052"/>
<area shape="rect" id="node76" href="mathcomp.solvable.alt.html" title="alt" alt="" coords="3077,2716,3149,2764"/>
<area shape="rect" id="node77" href="mathcomp.solvable.burnside_app.html" title="burnside_app" alt="" coords="3280,2812,3432,2860"/>
<area shape="rect" id="node78" href="mathcomp.solvable.center.html" title="center" alt="" coords="3213,2117,3294,2165"/>
<area shape="rect" id="node86" href="mathcomp.solvable.gseries.html" title="gseries" alt="" coords="3009,2230,3098,2278"/>
<area shape="rect" id="node79" href="mathcomp.solvable.commutator.html" title="commutator" alt="" coords="2977,2117,3116,2165"/>
<area shape="rect" id="node83" href="mathcomp.solvable.finmodule.html" title="finmodule" alt="" coords="3297,2230,3418,2278"/>
<area shape="rect" id="node91" href="mathcomp.solvable.pgroup.html" title="pgroup" alt="" coords="3490,2117,3579,2165"/>
<area shape="rect" id="node81" href="mathcomp.solvable.extraspecial.html" title="extraspecial" alt="" coords="3046,2812,3184,2860"/>
<area shape="rect" id="node84" href="mathcomp.solvable.frobenius.html" title="frobenius" alt="" coords="3528,2812,3640,2860"/>
<area shape="rect" id="node88" href="mathcomp.solvable.jordanholder.html" title="jordanholder" alt="" coords="2849,2422,2994,2470"/>
<area shape="rect" id="node90" href="mathcomp.solvable.nilpotent.html" title="nilpotent" alt="" coords="3151,2326,3260,2374"/>
<area shape="rect" id="node92" href="mathcomp.solvable.primitive_action.html" title="primitive_action" alt="" coords="3022,2614,3205,2662"/>
<area shape="rect" id="node87" href="mathcomp.solvable.hall.html" title="hall" alt="" coords="3365,2716,3437,2764"/>
<area shape="rect" id="node93" href="mathcomp.solvable.sylow.html" title="sylow" alt="" coords="3472,2422,3550,2470"/>
<area shape="rect" id="node94" href="mathcomp.boot.boot.html" title="boot" alt="" coords="503,1406,575,1454"/>
<area shape="rect" id="node95" href="mathcomp.boot.all_boot.html" title="all_boot" alt="" coords="488,1502,589,1550"/>
<area shape="rect" id="node122" href="mathcomp.ssreflect.all_ssreflect.html" title="all_ssreflect" alt="" coords="3808,1823,3947,1871"/>
<area shape="rect" id="node96" href="mathcomp.boot.bigop.html" title="bigop" alt="" coords="379,1063,456,1111"/>
<area shape="rect" id="node103" href="mathcomp.boot.finset.html" title="finset" alt="" coords="525,1159,600,1207"/>
<area shape="rect" id="node106" href="mathcomp.boot.monoid.html" title="monoid" alt="" coords="334,1159,429,1207"/>
<area shape="rect" id="node109" href="mathcomp.boot.prime.html" title="prime" alt="" coords="697,1159,775,1207"/>
<area shape="rect" id="node111" href="mathcomp.boot.ssrAC.html" title="ssrAC" alt="" coords="694,1261,775,1309"/>
<area shape="rect" id="node97" href="mathcomp.boot.binomial.html" title="binomial" alt="" coords="287,1261,396,1309"/>
<area shape="rect" id="node98" href="mathcomp.boot.choice.html" title="choice" alt="" coords="200,679,285,727"/>
<area shape="rect" id="node104" href="mathcomp.boot.fintype.html" title="fintype" alt="" coords="372,775,462,823"/>
<area shape="rect" id="node99" href="mathcomp.boot.div.html" title="div" alt="" coords="381,679,453,727"/>
<area shape="rect" id="node100" href="mathcomp.boot.eqtype.html" title="eqtype" alt="" coords="374,391,460,439"/>
<area shape="rect" id="node116" href="mathcomp.boot.ssrnat.html" title="ssrnat" alt="" coords="379,487,456,535"/>
<area shape="rect" id="node101" href="mathcomp.boot.finfun.html" title="finfun" alt="" coords="377,967,458,1015"/>
<area shape="rect" id="node102" href="mathcomp.boot.fingraph.html" title="fingraph" alt="" coords="126,967,229,1015"/>
<area shape="rect" id="node120" href="mathcomp.order.preorder.html" title="preorder" alt="" coords="3507,1615,3610,1663"/>
<area shape="rect" id="node105" href="mathcomp.boot.generic_quotient.html" title="generic_quotient" alt="" coords="589,1063,774,1111"/>
<area shape="rect" id="node118" href="mathcomp.boot.tuple.html" title="tuple" alt="" coords="381,871,453,919"/>
<area shape="rect" id="node107" href="mathcomp.boot.nmodule.html" title="nmodule" alt="" coords="492,1261,598,1309"/>
<area shape="rect" id="node108" href="mathcomp.boot.path.html" title="path" alt="" coords="549,679,621,727"/>
<area shape="rect" id="node110" href="mathcomp.boot.seq.html" title="seq" alt="" coords="381,583,453,631"/>
<area shape="rect" id="node112" href="mathcomp.boot.ssrbool.html" title="ssrbool" alt="" coords="372,295,462,343"/>
<area shape="rect" id="node113" href="mathcomp.boot.ssreflect.html" title="ssreflect" alt="" coords="122,103,224,151"/>
<area shape="rect" id="node114" href="mathcomp.boot.ssrfun.html" title="ssrfun" alt="" coords="378,199,457,247"/>
<area shape="rect" id="node115" href="mathcomp.boot.ssrmatching.html" title="ssrmatching" alt="" coords="320,103,458,151"/>
<area shape="rect" id="node117" href="mathcomp.boot.ssrnotations.html" title="ssrnotations" alt="" coords="554,103,691,151"/>
<area shape="rect" id="node119" href="mathcomp.order.all_order.html" title="all_order" alt="" coords="3504,1823,3613,1871"/>
<area shape="rect" id="node121" href="mathcomp.order.order.html" title="order" alt="" coords="3522,1711,3595,1759"/>
</map>
<div class="footer"><hr/>Generated by <a href="https://github.com/affeldt-aist/rocqnavi/">rocqnavi</a></div>
</div>
</div>
</main>
</body>
</html>