1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101
102. 102
103. 103
104. 104
105. 105
106. 106
107. 107
108. 108
109. 109
110. 110
111. 111
112. 112
113. 113
114. 114
115. 115
116. 116
117. 117
118. 118
119. 119
120. 120
121. 121
122. 122
123. 123
124. 124
125. 125
126. 126
127. 127
128. 128
129. 129
130. 130
131. 131
132. 132
133. 133
134. 134
135. 135
136. 136
137. 137
138. 138
139. 139
140. 140
141. 141
142. 142
143. 143
144. 144
145. 145
146. 146
147. 147
148. 148
149. 149
150. 150
151. 151
152. 152
153. 153
154. 154
155. 155
156. 156
157. 157
158. 158
159. 159
160. 160
161. 161
162. 162
163. 163
164. 164
165. 165
166. 166
167. 167
168. 168
169. 169
170. 170
171. 171
172. 172
173. 173
174. 174
175. 175
176. 176
177. 177
178. 178
179. 179
180. 180
181. 181
182. 182
183. 183
184. 184
185. 185
186. 186
187. 187
188. 188
189. 189
190. 190
191. 191
192. 192
193. 193
194. 194
195. 195
196. 196
197. 197
198. 198
199. 199
200. 200
201. 201
202. 202
203. 203
204. 204
205. 205
206. 206
207. 207
208. 208
209. 209
210. 210
211. 211
212. 212
213. 213
214. 214
215. 215
216. 216
217. 217
218. 218
219. 219
220. 220
221. 221
222. 222
223. 223
224. 224
225. 225
226. 226
227. 227
228. 228
229. 229
230. 230
231. 231
232. 232
233. 233
234. 234
235. 235
236. 236
237. 237
238. 238
239. 239
240. 240
241. 241
242. 242
243. 243
244. 244
245. 245
246. 246
247. 247
248. 248
249. 249
250. 250
251. 251
252. 252
253. 253
254. 254
255. 255
256. 256
257. 257
258. 258
259. 259
260. 260
261. 261
262. 262
263. 263
264. 264
265. 265
266. 266
267. 267
268. 268
269. 269
270. 270
271. 271
272. 272
273. 273
274. 274
275. 275
276. 276
277. 277
278. 278
279. 279
280. 280
281. 281
282. 282
283. 283
284. 284
285. 285
286. 286
287. 287
288. 288
289. 289
290. 290
291. 291
292. 292
293. 293
294. 294
295. 295
296. 296
297. 297
298. 298
299. 299
300. 300
301. 301
302. 302
303. 303
304. 304
305. 305
306. 306
307. 307
308. 308
309. 309
310. 310
311. 311
312. 312
313. 313
314. 314
315. 315
316. 316
317. 317
318. 318
319. 319
320. 320
321. 321
322. 322
323. 323
324. 324
325. 325
326. 326
327. 327
328. 328
329. 329
330. 330
331. 331
332. 332
333. 333
334. 334
335. 335
336. 336
337. 337
338. 338
339. 339
340. 340
341. 341
342. 342
343. 343
344. 344
345. 345
346. 346
347. 347
348. 348
349. 349
350. 350
351. 351
352. 352
353. 353
354. 354
355. 355
356. 356
357. 357
358. 358
359. 359
360. 360
361. 361
362. 362
363. 363
364. 364
365. 365
366. 366
367. 367
368. 368
369. 369
370. 370
371. 371
372. 372
373. 373
374. 374
375. 375
376. 376
377. 377
378. 378
379. 379
380. 380
381. 381
382. 382
383. 383
384. 384
385. 385
386. 386
387. 387
388. 388
389. 389
390. 390
391. 391
392. 392
393. 393
394. 394
395. 395
396. 396
397. 397
398. 398
399. 399
400. 400
401. 401
402. 402
403. 403
404. 404
405. 405
406. 406
407. 407
408. 408
409. 409
410. 410
411. 411
412. 412
413. 413
414. 414
415. 415
416. 416
417. 417
418. 418
419. 419
420. 420
421. 421
422. 422
423. 423
424. 424
425. 425
426. 426
427. 427
428. 428
429. 429
430. 430
431. 431
432. 432
433. 433
434. 434
435. 435
436. 436
437. 437
438. 438
439. 439
440. 440
441. 441
442. 442
443. 443
444. 444
445. 445
446. 446
447. 447
448. 448
449. 449
450. 450
451. 451
452. 452
453. 453
454. 454
455. 455
456. 456
457. 457
458. 458
459. 459
460. 460
461. 461
462. 462
463. 463
464. 464
465. 465
466. 466
467. 467
468. 468
469. 469
470. 470
471. 471
472. 472
473. 473
474. 474
475. 475
476. 476
477. 477
478. 478
479. 479
480. 480
481. 481
482. 482
483. 483
484. 484
485. 485
486. 486
487. 487
488. 488
489. 489
490. 490
491. 491
492. 492
493. 493
494. 494
495. 495
496. 496
497. 497
498. 498
499. 499
500. 500
501. 501
502. 502
503. 503
504. 504
505. 505
506. 506
507. 507
508. 508
509. 509
510. 510
511. 511
512. 512
513. 513
514. 514
515. 515
516. 516
517. 517
518. 518
519. 519
520. 520
521. 521
522. 522
523. 523
524. 524
525. 525
526. 526
527. 527
528. 528
529. 529
530. 530
531. 531
532. 532
533. 533
534. 534
535. 535
536. 536
537. 537
538. 538
539. 539
540. 540
541. 541
542. 542
543. 543
544. 544
545. 545
546. 546
547. 547
548. 548
549. 549
550. 550
551. 551
552. 552
553. 553
554. 554
555. 555
556. 556
557. 557
558. 558
559. 559
560. 560
561. 561
562. 562
563. 563
564. 564
565. 565
566. 566
567. 567
568. 568
569. 569
570. 570
571. 571
572. 572
573. 573
574. 574
575. 575
576. 576
577. 577
578. 578
579. 579
580. 580
581. 581
582. 582
583. 583

<!DOCTYPE html>
<html class="writer-html5" lang="en" data-content_root="./">
<head>
  <meta charset="utf-8" />
  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>Index &mdash; Mathematics in Lean v4.19.0 documentation</title>
      <link rel="stylesheet" type="text/css" href="_static/pygments.css?v=b86133f3" />
      <link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=e59714d7" />
      <link rel="stylesheet" type="text/css" href="_static/css/custom.css?v=0731ccc3" />

  
    <link rel="shortcut icon" href="_static/favicon.ico"/>
      <script src="_static/jquery.js?v=5d32c60e"></script>
      <script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
      <script src="_static/documentation_options.js?v=7048e04d"></script>
      <script src="_static/doctools.js?v=9bcbadda"></script>
      <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="#" />
    <link rel="search" title="Search" href="search.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >

          
          
          <a href="index.html" class="icon icon-home">
            Mathematics in Lean
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul>
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a></li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="C05_Elementary_Number_Theory.html">5. Elementary Number Theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="C06_Discrete_Mathematics.html">6. Discrete Mathematics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C07_Structures.html">7. Structures</a></li>
<li class="toctree-l1"><a class="reference internal" href="C08_Hierarchies.html">8. Hierarchies</a></li>
<li class="toctree-l1"><a class="reference internal" href="C09_Groups_and_Rings.html">9. Groups and Rings</a></li>
<li class="toctree-l1"><a class="reference internal" href="C10_Linear_Algebra.html">10. Linear algebra</a></li>
<li class="toctree-l1"><a class="reference internal" href="C11_Topology.html">11. Topology</a></li>
<li class="toctree-l1"><a class="reference internal" href="C12_Differential_Calculus.html">12. Differential Calculus</a></li>
<li class="toctree-l1"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html">13. Integration and Measure Theory</a></li>
</ul>
<ul class="current">
<li class="toctree-l1 current"><a class="current reference internal" href="#">Index</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">Mathematics in Lean</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home" aria-label="Home"></a></li>
      <li class="breadcrumb-item active">Index</li>
      <li class="wy-breadcrumbs-aside">
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             

<h1 id="index">Index</h1>

<div class="genindex-jumpbox">
 <a href="#A"><strong>A</strong></a>
 | <a href="#B"><strong>B</strong></a>
 | <a href="#C"><strong>C</strong></a>
 | <a href="#D"><strong>D</strong></a>
 | <a href="#E"><strong>E</strong></a>
 | <a href="#F"><strong>F</strong></a>
 | <a href="#G"><strong>G</strong></a>
 | <a href="#H"><strong>H</strong></a>
 | <a href="#I"><strong>I</strong></a>
 | <a href="#L"><strong>L</strong></a>
 | <a href="#M"><strong>M</strong></a>
 | <a href="#N"><strong>N</strong></a>
 | <a href="#O"><strong>O</strong></a>
 | <a href="#P"><strong>P</strong></a>
 | <a href="#R"><strong>R</strong></a>
 | <a href="#S"><strong>S</strong></a>
 | <a href="#T"><strong>T</strong></a>
 | <a href="#U"><strong>U</strong></a>
 | <a href="#V"><strong>V</strong></a>
 
</div>
<h2 id="A">A</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C09_Groups_and_Rings.html#index-3">abel</a>
</li>
      <li><a href="C02_Basics.html#index-24">absolute value</a>
</li>
      <li><a href="C03_Logic.html#index-17">absurd</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-7">anonymous constructor</a>
</li>
      <li><a href="C02_Basics.html#index-12">apply</a>, <a href="C02_Basics.html#index-17">[1]</a>
</li>
      <li><a href="C03_Logic.html#index-19">assumption</a>
</li>
  </ul></td>
</tr></table>

<h2 id="B">B</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C04_Sets_and_Functions.html#index-3">bounded quantifiers</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-23">by_cases</a>
</li>
      <li><a href="C03_Logic.html#index-14">by_contra</a>
</li>
  </ul></td>
</tr></table>

<h2 id="C">C</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-3">calc</a>
</li>
      <li><a href="C03_Logic.html#index-8">cases</a>
</li>
      <li><a href="C03_Logic.html#index-2">change</a>
</li>
      <li><a href="C01_Introduction.html#index-0">check</a>
</li>
      <li>
    command

      <ul>
        <li><a href="C02_Basics.html#index-9">open</a>
</li>
      </ul></li>
      <li>
    commands

      <ul>
        <li><a href="C01_Introduction.html#index-0">check</a>
</li>
      </ul></li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-8">commutative ring</a>
</li>
      <li><a href="C03_Logic.html#index-25">congr</a>
</li>
      <li><a href="C03_Logic.html#index-18">constructor</a>
</li>
      <li><a href="C11_Topology.html#index-3">continuity</a>
</li>
      <li><a href="C03_Logic.html#index-17">contradiction</a>
</li>
      <li><a href="C03_Logic.html#index-16">contrapose</a>
</li>
      <li><a href="C03_Logic.html#index-26">convert</a>
</li>
  </ul></td>
</tr></table>

<h2 id="D">D</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C05_Elementary_Number_Theory.html#index-0">decide</a>
</li>
      <li><a href="C02_Basics.html#index-13">definitional equality</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C12_Differential_Calculus.html#index-0">differential calculus</a>
</li>
      <li><a href="C02_Basics.html#index-25">divisibility</a>
</li>
      <li><a href="C03_Logic.html#index-2">dsimp</a>
</li>
  </ul></td>
</tr></table>

<h2 id="E">E</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C12_Differential_Calculus.html#index-1">elementary calculus</a>
</li>
      <li><a href="C03_Logic.html#index-4">erw</a>
</li>
      <li><a href="C02_Basics.html#index-12">exact</a>, <a href="C02_Basics.html#index-17">[1]</a>, <a href="C02_Basics.html#index-5">[2]</a>
</li>
      <li><a href="C03_Logic.html#index-22">excluded middle</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-17">exfalso</a>
</li>
      <li><a href="C02_Basics.html#index-19">exponential</a>
</li>
      <li><a href="C03_Logic.html#index-24">ext</a>
</li>
      <li><a href="C03_Logic.html#index-24">extensionality</a>
</li>
  </ul></td>
</tr></table>

<h2 id="F">F</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-11">field_simp</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C11_Topology.html#index-1">Filter</a>
</li>
      <li><a href="C03_Logic.html#index-12">from</a>
</li>
  </ul></td>
</tr></table>

<h2 id="G">G</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-26">gcd</a>
</li>
      <li><a href="C02_Basics.html#index-2">goal</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-14">group (algebraic structure)</a>, <a href="C09_Groups_and_Rings.html#index-1">[1]</a>

      <ul>
        <li><a href="C02_Basics.html#index-15">(tactic)</a>, <a href="C09_Groups_and_Rings.html#index-2">[1]</a>
</li>
      </ul></li>
  </ul></td>
</tr></table>

<h2 id="H">H</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-11">have</a>, <a href="C03_Logic.html#index-12">[1]</a>
</li>
  </ul></td>
</tr></table>

<h2 id="I">I</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-10">implicit argument</a>
</li>
      <li><a href="C02_Basics.html#index-16">inequalities</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-5">injective function</a>
</li>
      <li><a href="C13_Integration_and_Measure_Theory.html#index-0">integration</a>, <a href="C13_Integration_and_Measure_Theory.html#index-1">[1]</a>
</li>
      <li><a href="C03_Logic.html#index-0">intro</a>
</li>
  </ul></td>
</tr></table>

<h2 id="L">L</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-1">lambda abstraction</a>
</li>
      <li><a href="C02_Basics.html#index-28">lattice</a>
</li>
      <li><a href="C02_Basics.html#index-26">lcm</a>
</li>
      <li><a href="C03_Logic.html#index-21">left</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-13">let</a>
</li>
      <li><a href="C02_Basics.html#index-18">linarith</a>
</li>
      <li><a href="C10_Linear_Algebra.html#index-1">linear map</a>
</li>
      <li><a href="C02_Basics.html#index-2">local context</a>
</li>
      <li><a href="C02_Basics.html#index-19">logarithm</a>
</li>
  </ul></td>
</tr></table>

<h2 id="M">M</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C10_Linear_Algebra.html#index-3">matrices</a>
</li>
      <li><a href="C02_Basics.html#index-21">max</a>
</li>
      <li><a href="C13_Integration_and_Measure_Theory.html#index-2">measure theory</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-30">metric space</a>, <a href="C11_Topology.html#index-2">[1]</a>
</li>
      <li><a href="C02_Basics.html#index-21">min</a>
</li>
      <li><a href="C09_Groups_and_Rings.html#index-0">monoid</a>
</li>
      <li><a href="C03_Logic.html#index-3">monotone function</a>
</li>
  </ul></td>
</tr></table>

<h2 id="N">N</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-9">namespace</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-20">norm_num</a>
</li>
      <li><a href="C12_Differential_Calculus.html#index-2">normed space</a>
</li>
  </ul></td>
</tr></table>

<h2 id="O">O</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-9">open</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-27">order relation</a>
</li>
  </ul></td>
</tr></table>

<h2 id="P">P</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-27">partial order</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C02_Basics.html#index-2">proof state</a>
</li>
      <li><a href="C03_Logic.html#index-15">push_neg</a>
</li>
  </ul></td>
</tr></table>

<h2 id="R">R</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-9">rcases</a>
</li>
      <li><a href="C02_Basics.html#index-1">real numbers</a>
</li>
      <li><a href="C02_Basics.html#index-13">reflexivity</a>
</li>
      <li><a href="C02_Basics.html#index-23">repeat</a>
</li>
      <li><a href="C02_Basics.html#index-0">rewrite</a>
</li>
      <li><a href="C02_Basics.html#index-13">rfl</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-21">right</a>
</li>
      <li><a href="C02_Basics.html#index-7">ring (algebraic structure)</a>, <a href="C09_Groups_and_Rings.html#index-4">[1]</a>

      <ul>
        <li><a href="C02_Basics.html#index-6">(tactic)</a>
</li>
      </ul></li>
      <li><a href="C03_Logic.html#index-9">rintro</a>
</li>
      <li><a href="C02_Basics.html#index-0">rw</a>, <a href="C02_Basics.html#index-4">[1]</a>
</li>
      <li><a href="C04_Sets_and_Functions.html#index-2">rwa</a>
</li>
  </ul></td>
</tr></table>

<h2 id="S">S</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C04_Sets_and_Functions.html#index-0">set operations</a>
</li>
      <li><a href="C02_Basics.html#index-22">show</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-20">simp</a>, <a href="C04_Sets_and_Functions.html#index-1">[1]</a>
</li>
      <li><a href="C03_Logic.html#index-10">surjective function</a>
</li>
  </ul></td>
</tr></table>

<h2 id="T">T</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li>
    tactics

      <ul>
        <li><a href="C02_Basics.html#index-15">abel</a>, <a href="C09_Groups_and_Rings.html#index-3">[1]</a>
</li>
        <li><a href="C02_Basics.html#index-12">apply</a>, <a href="C02_Basics.html#index-17">[1]</a>
</li>
        <li><a href="C03_Logic.html#index-19">assumption</a>
</li>
        <li><a href="C03_Logic.html#index-23">by_cases</a>
</li>
        <li><a href="C03_Logic.html#index-14">by_contra and by_contradiction</a>
</li>
        <li><a href="C02_Basics.html#index-3">calc</a>
</li>
        <li><a href="C03_Logic.html#index-8">cases</a>
</li>
        <li><a href="C03_Logic.html#index-2">change</a>
</li>
        <li><a href="C03_Logic.html#index-25">congr</a>
</li>
        <li><a href="C03_Logic.html#index-18">constructor</a>
</li>
        <li><a href="C11_Topology.html#index-3">continuity</a>
</li>
        <li><a href="C03_Logic.html#index-17">contradiction</a>
</li>
        <li><a href="C03_Logic.html#index-16">contrapose</a>
</li>
        <li><a href="C03_Logic.html#index-26">convert</a>
</li>
        <li><a href="C05_Elementary_Number_Theory.html#index-0">decide</a>
</li>
        <li><a href="C03_Logic.html#index-2">dsimp</a>
</li>
        <li><a href="C03_Logic.html#index-4">erw</a>
</li>
        <li><a href="C02_Basics.html#index-12">exact</a>, <a href="C02_Basics.html#index-17">[1]</a>, <a href="C02_Basics.html#index-5">[2]</a>
</li>
        <li><a href="C03_Logic.html#index-17">exfalso</a>
</li>
        <li><a href="C03_Logic.html#index-24">ext</a>
</li>
        <li><a href="C03_Logic.html#index-11">field_simp</a>
</li>
        <li><a href="C03_Logic.html#index-12">from</a>
</li>
        <li><a href="C02_Basics.html#index-15">group</a>, <a href="C09_Groups_and_Rings.html#index-2">[1]</a>
</li>
        <li><a href="C02_Basics.html#index-11">have</a>, <a href="C03_Logic.html#index-12">[1]</a>
</li>
        <li><a href="C03_Logic.html#index-0">intro</a>
</li>
        <li><a href="C03_Logic.html#index-21">left</a>
</li>
        <li><a href="C03_Logic.html#index-13">let</a>
</li>
        <li><a href="C02_Basics.html#index-18">linarith</a>
</li>
        <li><a href="C02_Basics.html#index-15">noncomm_ring</a>
</li>
        <li><a href="C02_Basics.html#index-20">norm_num</a>
</li>
        <li><a href="C03_Logic.html#index-15">push_neg</a>
</li>
        <li><a href="C03_Logic.html#index-9">rcases</a>
</li>
        <li><a href="C02_Basics.html#index-13">refl and reflexivity</a>
</li>
        <li><a href="C02_Basics.html#index-23">repeat</a>
</li>
        <li><a href="C03_Logic.html#index-21">right</a>
</li>
        <li><a href="C02_Basics.html#index-6">ring</a>
</li>
        <li><a href="C03_Logic.html#index-9">rintro</a>
</li>
        <li><a href="C02_Basics.html#index-0">rw and rewrite</a>, <a href="C02_Basics.html#index-4">[1]</a>
</li>
        <li><a href="C04_Sets_and_Functions.html#index-2">rwa</a>
</li>
        <li><a href="C02_Basics.html#index-22">show</a>
</li>
        <li><a href="C03_Logic.html#index-20">simp</a>, <a href="C04_Sets_and_Functions.html#index-1">[1]</a>
</li>
        <li><a href="C02_Basics.html#index-29">trans</a>
</li>
        <li><a href="C03_Logic.html#index-6">use</a>
</li>
      </ul></li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-12">this</a>
</li>
      <li><a href="C11_Topology.html#index-4">topological space</a>
</li>
      <li><a href="C11_Topology.html#index-0">topology</a>
</li>
      <li><a href="C02_Basics.html#index-29">trans</a>
</li>
  </ul></td>
</tr></table>

<h2 id="U">U</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C03_Logic.html#index-6">use</a>
</li>
  </ul></td>
</tr></table>

<h2 id="V">V</h2>
<table style="width: 100%" class="indextable genindextable"><tr>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C10_Linear_Algebra.html#index-0">vector space</a>
</li>
  </ul></td>
  <td style="width: 33%; vertical-align: top;"><ul>
      <li><a href="C10_Linear_Algebra.html#index-2">vector subspace</a>
</li>
  </ul></td>
</tr></table>



           </div>
          </div>
          <footer>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2020-2025, Jeremy Avigad, Patrick Massot. Text licensed under CC BY 4.0.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>