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
584. 584
585. 585
586. 586
587. 587
588. 588
589. 589
590. 590
591. 591
592. 592
593. 593
594. 594
595. 595
596. 596
597. 597
598. 598
599. 599
600. 600
601. 601
602. 602
603. 603
604. 604
605. 605
606. 606
607. 607
608. 608
609. 609
610. 610
611. 611
612. 612
613. 613
614. 614
615. 615
616. 616
617. 617
618. 618
619. 619
620. 620
621. 621
622. 622
623. 623
624. 624
625. 625
626. 626
627. 627
628. 628
629. 629
630. 630
631. 631
632. 632
633. 633
634. 634
635. 635
636. 636
637. 637
638. 638
639. 639
640. 640
641. 641
642. 642
643. 643
644. 644
645. 645
646. 646
647. 647
648. 648
649. 649
650. 650
651. 651
652. 652
653. 653
654. 654
655. 655
656. 656
657. 657
658. 658
659. 659
660. 660
661. 661
662. 662
663. 663
664. 664
665. 665
666. 666
667. 667
668. 668
669. 669
670. 670
671. 671
672. 672
673. 673
674. 674
675. 675
676. 676
677. 677
678. 678
679. 679
680. 680
681. 681
682. 682
683. 683
684. 684
685. 685
686. 686
687. 687
688. 688
689. 689
690. 690
691. 691
692. 692
693. 693
694. 694
695. 695
696. 696
697. 697
698. 698
699. 699
700. 700
701. 701
702. 702
703. 703
704. 704
705. 705
706. 706
707. 707
708. 708
709. 709
710. 710
711. 711
712. 712
713. 713
714. 714
715. 715
716. 716
717. 717
718. 718
719. 719
720. 720
721. 721
722. 722
723. 723
724. 724
725. 725
726. 726
727. 727
728. 728
729. 729
730. 730
731. 731
732. 732
733. 733
734. 734
735. 735
736. 736
737. 737
738. 738
739. 739
740. 740
741. 741
742. 742
743. 743
744. 744
745. 745
746. 746
747. 747
748. 748
749. 749
750. 750
751. 751
752. 752
753. 753
754. 754
755. 755
756. 756
757. 757
758. 758
759. 759
760. 760
761. 761
762. 762
763. 763
764. 764
765. 765
766. 766
767. 767
768. 768
769. 769
770. 770
771. 771
772. 772
773. 773
774. 774
775. 775
776. 776
777. 777
778. 778
779. 779
780. 780
781. 781
782. 782
783. 783
784. 784
785. 785
786. 786
787. 787
788. 788
789. 789
790. 790
791. 791
792. 792
793. 793
794. 794
795. 795
796. 796
797. 797
798. 798
799. 799
800. 800
801. 801
802. 802
803. 803
804. 804
805. 805
806. 806
807. 807
808. 808
809. 809
810. 810
811. 811
812. 812
813. 813
814. 814
815. 815
816. 816
817. 817
818. 818
819. 819
820. 820
821. 821
822. 822
823. 823
824. 824
825. 825
826. 826
827. 827
828. 828
829. 829
830. 830
831. 831
832. 832
833. 833
834. 834
835. 835
836. 836
837. 837
838. 838
839. 839
840. 840
841. 841
842. 842
843. 843
844. 844
845. 845
846. 846
847. 847
848. 848
849. 849
850. 850
851. 851
852. 852
853. 853
854. 854
855. 855
856. 856
857. 857
858. 858
859. 859
860. 860
861. 861
862. 862
863. 863
864. 864
865. 865
866. 866
867. 867
868. 868
869. 869
870. 870
871. 871
872. 872
873. 873
874. 874
875. 875
876. 876
877. 877
878. 878
879. 879
880. 880
881. 881
882. 882
883. 883
884. 884
885. 885
886. 886
887. 887
888. 888
889. 889
890. 890
891. 891
892. 892
893. 893
894. 894
895. 895
896. 896
897. 897
898. 898
899. 899
900. 900
901. 901
902. 902
903. 903
904. 904
905. 905
906. 906
907. 907
908. 908
909. 909
910. 910
911. 911
912. 912
913. 913
914. 914
915. 915
916. 916
917. 917
918. 918
919. 919
920. 920
921. 921
922. 922
923. 923
924. 924
925. 925
926. 926
927. 927
928. 928
929. 929
930. 930
931. 931
932. 932
933. 933
934. 934
935. 935
936. 936
937. 937
938. 938
939. 939
940. 940
941. 941
942. 942
943. 943
944. 944
945. 945
946. 946
947. 947
948. 948
949. 949
950. 950
951. 951
952. 952
953. 953
954. 954
955. 955
956. 956
957. 957
958. 958
959. 959
960. 960
961. 961
962. 962
963. 963
964. 964
965. 965
966. 966
967. 967
968. 968
969. 969
970. 970
971. 971
972. 972
973. 973
974. 974
975. 975
976. 976
977. 977
978. 978
979. 979
980. 980
981. 981
982. 982
983. 983
984. 984
985. 985
986. 986
987. 987
988. 988
989. 989
990. 990
991. 991
992. 992
993. 993
994. 994
995. 995
996. 996
997. 997
998. 998
999. 999
1000. 1000
1001. 1001
1002. 1002
1003. 1003
1004. 1004
1005. 1005
1006. 1006
1007. 1007
1008. 1008
1009. 1009
1010. 1010
1011. 1011
1012. 1012
1013. 1013
1014. 1014
1015. 1015
1016. 1016
1017. 1017
1018. 1018
1019. 1019
1020. 1020
1021. 1021
1022. 1022
1023. 1023
1024. 1024
1025. 1025
1026. 1026
1027. 1027
1028. 1028
1029. 1029
1030. 1030
1031. 1031
1032. 1032
1033. 1033
1034. 1034
1035. 1035
1036. 1036
1037. 1037
1038. 1038
1039. 1039
1040. 1040
1041. 1041
1042. 1042
1043. 1043
1044. 1044
1045. 1045
1046. 1046
1047. 1047
1048. 1048
1049. 1049
1050. 1050
1051. 1051
1052. 1052
1053. 1053
1054. 1054
1055. 1055
1056. 1056
1057. 1057
1058. 1058
1059. 1059
1060. 1060
1061. 1061
1062. 1062
1063. 1063
1064. 1064
1065. 1065
1066. 1066
1067. 1067
1068. 1068
1069. 1069
1070. 1070
1071. 1071
1072. 1072
1073. 1073
1074. 1074
1075. 1075
1076. 1076
1077. 1077
1078. 1078
1079. 1079
1080. 1080
1081. 1081
1082. 1082
1083. 1083
1084. 1084
1085. 1085
1086. 1086
1087. 1087
1088. 1088
1089. 1089
1090. 1090
1091. 1091
1092. 1092
1093. 1093
1094. 1094
1095. 1095
1096. 1096
1097. 1097
1098. 1098
1099. 1099
1100. 1100
1101. 1101
1102. 1102
1103. 1103
1104. 1104
1105. 1105
1106. 1106
1107. 1107
1108. 1108
1109. 1109
1110. 1110
1111. 1111
1112. 1112
1113. 1113
1114. 1114
1115. 1115
1116. 1116
1117. 1117
1118. 1118
1119. 1119
1120. 1120
1121. 1121
1122. 1122
1123. 1123
1124. 1124
1125. 1125
1126. 1126
1127. 1127
1128. 1128
1129. 1129
1130. 1130
1131. 1131
1132. 1132
1133. 1133
1134. 1134
1135. 1135
1136. 1136
1137. 1137
1138. 1138
1139. 1139
1140. 1140
1141. 1141
1142. 1142
1143. 1143
1144. 1144
1145. 1145
1146. 1146
1147. 1147
1148. 1148
1149. 1149
1150. 1150
1151. 1151
1152. 1152
1153. 1153
1154. 1154
1155. 1155
1156. 1156
1157. 1157
1158. 1158
1159. 1159
1160. 1160
1161. 1161
1162. 1162
1163. 1163
1164. 1164
1165. 1165
1166. 1166
1167. 1167
1168. 1168
1169. 1169
1170. 1170
1171. 1171
1172. 1172
1173. 1173
1174. 1174
1175. 1175
1176. 1176
1177. 1177
1178. 1178
1179. 1179
1180. 1180
1181. 1181
1182. 1182
1183. 1183
1184. 1184
1185. 1185
1186. 1186
1187. 1187
1188. 1188
1189. 1189
1190. 1190
1191. 1191
1192. 1192
1193. 1193
1194. 1194
1195. 1195
1196. 1196
1197. 1197
1198. 1198
1199. 1199
1200. 1200
1201. 1201
1202. 1202
1203. 1203
1204. 1204
1205. 1205
1206. 1206
1207. 1207
1208. 1208
1209. 1209
1210. 1210
1211. 1211
1212. 1212
1213. 1213
1214. 1214
1215. 1215
1216. 1216
1217. 1217
1218. 1218
1219. 1219
1220. 1220
1221. 1221
1222. 1222
1223. 1223
1224. 1224
1225. 1225
1226. 1226
1227. 1227
1228. 1228
1229. 1229
1230. 1230
1231. 1231
1232. 1232
1233. 1233
1234. 1234
1235. 1235
1236. 1236
1237. 1237
1238. 1238
1239. 1239
1240. 1240
1241. 1241
1242. 1242
1243. 1243
1244. 1244
1245. 1245
1246. 1246
1247. 1247
1248. 1248
1249. 1249
1250. 1250
1251. 1251
1252. 1252
1253. 1253
1254. 1254
1255. 1255
1256. 1256
1257. 1257
1258. 1258
1259. 1259
1260. 1260
1261. 1261
1262. 1262
1263. 1263
1264. 1264
1265. 1265
1266. 1266
1267. 1267
1268. 1268
1269. 1269
1270. 1270
1271. 1271
1272. 1272
1273. 1273
1274. 1274
1275. 1275
1276. 1276
1277. 1277
1278. 1278
1279. 1279
1280. 1280
1281. 1281
1282. 1282
1283. 1283
1284. 1284
1285. 1285
1286. 1286
1287. 1287
1288. 1288
1289. 1289
1290. 1290
1291. 1291
1292. 1292
1293. 1293
1294. 1294
1295. 1295
1296. 1296
1297. 1297
1298. 1298
1299. 1299
1300. 1300
1301. 1301
1302. 1302
1303. 1303
1304. 1304
1305. 1305
1306. 1306
1307. 1307
1308. 1308
1309. 1309
1310. 1310
1311. 1311
1312. 1312
1313. 1313
1314. 1314
1315. 1315
1316. 1316
1317. 1317
1318. 1318
1319. 1319
1320. 1320
1321. 1321
1322. 1322
1323. 1323
1324. 1324
1325. 1325
1326. 1326
1327. 1327
1328. 1328
1329. 1329
1330. 1330
1331. 1331
1332. 1332
1333. 1333
1334. 1334
1335. 1335
1336. 1336
1337. 1337
1338. 1338
1339. 1339
1340. 1340
1341. 1341
1342. 1342
1343. 1343
1344. 1344
1345. 1345
1346. 1346
1347. 1347
1348. 1348
1349. 1349
1350. 1350
1351. 1351
1352. 1352
1353. 1353
1354. 1354
1355. 1355
1356. 1356
1357. 1357
1358. 1358
1359. 1359
1360. 1360
1361. 1361
1362. 1362
1363. 1363
1364. 1364
1365. 1365
1366. 1366
1367. 1367
1368. 1368
1369. 1369
1370. 1370
1371. 1371
1372. 1372
1373. 1373
1374. 1374
1375. 1375
1376. 1376
1377. 1377
1378. 1378
1379. 1379
1380. 1380
1381. 1381
1382. 1382
1383. 1383
1384. 1384
1385. 1385
1386. 1386
1387. 1387
1388. 1388
1389. 1389
1390. 1390
1391. 1391
1392. 1392
1393. 1393
1394. 1394
1395. 1395
1396. 1396
1397. 1397
1398. 1398
1399. 1399
1400. 1400
1401. 1401
1402. 1402
1403. 1403
1404. 1404
1405. 1405
1406. 1406
1407. 1407
1408. 1408
1409. 1409
1410. 1410
1411. 1411
1412. 1412
1413. 1413
1414. 1414
1415. 1415
1416. 1416
1417. 1417
1418. 1418
1419. 1419
1420. 1420
1421. 1421
1422. 1422
1423. 1423
1424. 1424
1425. 1425
1426. 1426
1427. 1427
1428. 1428
1429. 1429
1430. 1430
1431. 1431
1432. 1432
1433. 1433
1434. 1434
1435. 1435
1436. 1436
1437. 1437
1438. 1438
1439. 1439
1440. 1440
1441. 1441
1442. 1442
1443. 1443
1444. 1444
1445. 1445
1446. 1446
1447. 1447
1448. 1448
1449. 1449
1450. 1450
1451. 1451
1452. 1452
1453. 1453
1454. 1454
1455. 1455
1456. 1456
1457. 1457
1458. 1458
1459. 1459
1460. 1460
1461. 1461
1462. 1462
1463. 1463
1464. 1464
1465. 1465
1466. 1466
1467. 1467
1468. 1468
1469. 1469
1470. 1470
1471. 1471
1472. 1472
1473. 1473
1474. 1474
1475. 1475
1476. 1476
1477. 1477
1478. 1478
1479. 1479
1480. 1480
1481. 1481
1482. 1482
1483. 1483
1484. 1484
1485. 1485
1486. 1486
1487. 1487
1488. 1488
1489. 1489
1490. 1490
1491. 1491
1492. 1492
1493. 1493
1494. 1494
1495. 1495
1496. 1496
1497. 1497
1498. 1498
1499. 1499
1500. 1500
1501. 1501
1502. 1502
1503. 1503
1504. 1504
1505. 1505
1506. 1506
1507. 1507
1508. 1508
1509. 1509
1510. 1510
1511. 1511
1512. 1512
1513. 1513
1514. 1514
1515. 1515
1516. 1516
1517. 1517
1518. 1518
1519. 1519
1520. 1520
1521. 1521
1522. 1522
1523. 1523
1524. 1524
1525. 1525
1526. 1526
1527. 1527
1528. 1528
1529. 1529
1530. 1530
1531. 1531
1532. 1532
1533. 1533
1534. 1534
1535. 1535
1536. 1536
1537. 1537
1538. 1538
1539. 1539
1540. 1540
1541. 1541
1542. 1542
1543. 1543
1544. 1544
1545. 1545
1546. 1546
1547. 1547
1548. 1548
1549. 1549
1550. 1550
1551. 1551
1552. 1552
1553. 1553
1554. 1554
1555. 1555
1556. 1556
1557. 1557
1558. 1558
1559. 1559
1560. 1560
1561. 1561
1562. 1562

<!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" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>7. Structures &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 async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="8. Hierarchies" href="C08_Hierarchies.html" />
    <link rel="prev" title="6. Discrete Mathematics" href="C06_Discrete_Mathematics.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 class="current">
<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 current"><a class="current reference internal" href="#">7. Structures</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#defining-structures">7.1. Defining structures</a></li>
<li class="toctree-l2"><a class="reference internal" href="#algebraic-structures">7.2. Algebraic Structures</a></li>
<li class="toctree-l2"><a class="reference internal" href="#building-the-gaussian-integers">7.3. Building the Gaussian Integers</a></li>
</ul>
</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>
<li class="toctree-l1"><a class="reference internal" href="genindex.html">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"><span class="section-number">7. </span>Structures</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/C07_Structures.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="structures">
<span id="id1"></span><h1><span class="section-number">7. </span>Structures<a class="headerlink" href="#structures" title="Link to this heading">&#61633;</a></h1>
<p>Modern mathematics makes essential use of algebraic
structures,
which encapsulate patterns that can be instantiated in
multiple settings.
The subject provides various ways of defining such structures and
constructing particular instances.</p>
<p>Lean therefore provides corresponding ways of
defining structures formally and working with them.
You have already seen examples of algebraic structures in Lean,
such as rings and lattices, which were discussed in
<a class="reference internal" href="C02_Basics.html#basics"><span class="std std-numref">Chapter 2</span></a>.
This chapter will explain the mysterious square bracket annotations
that you saw there,
<code class="docutils literal notranslate"><span class="pre">[Ring</span> <span class="pre">&#945;]</span></code> and <code class="docutils literal notranslate"><span class="pre">[Lattice</span> <span class="pre">&#945;]</span></code>.
It will also show you how to define and use
algebraic structures on your own.</p>
<p>For more technical detail, you can consult <a class="reference external" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem Proving in Lean</a>,
and a paper by Anne Baanen, <a class="reference external" href="https://arxiv.org/abs/2202.01629">Use and abuse of instance parameters in the Lean mathematical library</a>.</p>
<section id="defining-structures">
<span id="section-structures"></span><h2><span class="section-number">7.1. </span>Defining structures<a class="headerlink" href="#defining-structures" title="Link to this heading">&#61633;</a></h2>
<p>In the broadest sense of the term, a <em>structure</em> is a specification
of a collection of data, possibly with constraints that the
data is required to satisfy.
An <em>instance</em> of the structure is a particular bundle of data satisfying
the constraints. For example, we can specify that a point is
a tuple of three real numbers:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[</span><span class="n">ext</span><span class="kd">]</span>
<span class="kd">structure</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
</pre></div>
</div>
<p>The <code class="docutils literal notranslate"><span class="pre">&#64;[ext]</span></code> annotation tells Lean to automatically generate theorems
that can be used to prove that two instances of a structure are equal
when their components are equal, a property known as <em>extensionality</em>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">Point.ext</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hx</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a.x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b.x</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hy</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a.y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b.y</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hz</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a.z</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b.z</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">ext</span>
<span class="w">  </span><span class="n">repeat&#39;</span><span class="w"> </span><span class="n">assumption</span>
</pre></div>
</div>
<p>We can then define particular instances of the <code class="docutils literal notranslate"><span class="pre">Point</span></code> structure.
Lean provides multiple ways of doing that.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">myPoint1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="mi">2</span>
<span class="w">  </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="bp">-</span><span class="mi">1</span>
<span class="w">  </span><span class="n">z</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="mi">4</span>

<span class="kd">def</span><span class="w"> </span><span class="n">myPoint2</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="bp">-</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">&#10217;</span>

<span class="kd">def</span><span class="w"> </span><span class="n">myPoint3</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Point.mk</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">(</span><span class="bp">-</span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="mi">4</span>
</pre></div>
</div>
<p>In the first example, the fields of the structure are named
explicitly.
The function <code class="docutils literal notranslate"><span class="pre">Point.mk</span></code> referred to in the definition of <code class="docutils literal notranslate"><span class="pre">myPoint3</span></code>
is known as the <em>constructor</em> for the <code class="docutils literal notranslate"><span class="pre">Point</span></code> structure, because
it serves to construct elements.
You can specify a different name if you want, like <code class="docutils literal notranslate"><span class="pre">build</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">structure</span><span class="w"> </span><span class="n">Point&#39;</span><span class="w"> </span><span class="n">where</span><span class="w"> </span><span class="n">build</span><span class="w"> </span><span class="o">::</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Point&#39;.build</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">(</span><span class="bp">-</span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="mi">4</span>
</pre></div>
</div>
<p>The next two examples show how to define functions on structures.
Whereas the second example makes the <code class="docutils literal notranslate"><span class="pre">Point.mk</span></code>
constructor explicit, the first example uses an anonymous constructor
for brevity.
Lean can infer the relevant constructor from the indicated type of
<code class="docutils literal notranslate"><span class="pre">add</span></code>.
It is conventional to put definitions and theorems associated
with a structure like <code class="docutils literal notranslate"><span class="pre">Point</span></code> in a namespace with the same name.
In the example below, because we have opened the <code class="docutils literal notranslate"><span class="pre">Point</span></code>
namespace, the full name of <code class="docutils literal notranslate"><span class="pre">add</span></code> is <code class="docutils literal notranslate"><span class="pre">Point.add</span></code>.
When the namespace is not open, we have to use the full name.
But remember that it is often convenient to use
anonymous projection notation,
which allows us to write <code class="docutils literal notranslate"><span class="pre">a.add</span> <span class="pre">b</span></code> instead of <code class="docutils literal notranslate"><span class="pre">Point.add</span> <span class="pre">a</span> <span class="pre">b</span></code>.
Lean interprets the former as the latter because <code class="docutils literal notranslate"><span class="pre">a</span></code> has type <code class="docutils literal notranslate"><span class="pre">Point</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">namespace</span><span class="w"> </span><span class="n">Point</span>

<span class="kd">def</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="n">a.x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.x</span><span class="o">,</span><span class="w"> </span><span class="n">a.y</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.y</span><span class="o">,</span><span class="w"> </span><span class="n">a.z</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.z</span><span class="o">&#10217;</span>

<span class="kd">def</span><span class="w"> </span><span class="n">add&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.x</span>
<span class="w">  </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.y</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.y</span>
<span class="w">  </span><span class="n">z</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.z</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.z</span>

<span class="k">#check</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">myPoint1</span><span class="w"> </span><span class="n">myPoint2</span>
<span class="k">#check</span><span class="w"> </span><span class="n">myPoint1.add</span><span class="w"> </span><span class="n">myPoint2</span>

<span class="kd">end</span><span class="w"> </span><span class="n">Point</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Point.add</span><span class="w"> </span><span class="n">myPoint1</span><span class="w"> </span><span class="n">myPoint2</span>
<span class="k">#check</span><span class="w"> </span><span class="n">myPoint1.add</span><span class="w"> </span><span class="n">myPoint2</span>
</pre></div>
</div>
<p>Below we will continue to put definitions in the relevant
namespace, but we will leave the namespacing commands out of the quoted
snippets. To prove properties of the addition function,
we can use <code class="docutils literal notranslate"><span class="pre">rw</span></code> to expand the definition and <code class="docutils literal notranslate"><span class="pre">ext</span></code> to
reduce an equation between two elements of the structure to equations
between the components.
Below we use the <code class="docutils literal notranslate"><span class="pre">protected</span></code> keyword so that the name of the
theorem is <code class="docutils literal notranslate"><span class="pre">Point.add_comm</span></code>, even when the namespace is open.
This is helpful when we want to avoid ambiguity with a generic
theorem like <code class="docutils literal notranslate"><span class="pre">add_comm</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">protected</span><span class="w"> </span><span class="kd">theorem</span><span class="w"> </span><span class="n">add_comm</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add</span><span class="o">,</span><span class="w"> </span><span class="n">add</span><span class="o">]</span>
<span class="w">  </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">dsimp</span>
<span class="w">  </span><span class="n">repeat&#39;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">add_comm</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">add</span><span class="o">,</span><span class="w"> </span><span class="n">add_comm</span><span class="o">]</span>
</pre></div>
</div>
<p>Because Lean can unfold definitions and simplify projections
internally, sometimes the equations we want hold definitionally.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">add_x</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a.add</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="bp">.</span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a.x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>It is also possible to define functions on structures using
pattern matching,
in a manner similar to the way we defined recursive functions in
<a class="reference internal" href="C05_Elementary_Number_Theory.html#section-induction-and-recursion"><span class="std std-numref">Section 5.2</span></a>.
The definitions <code class="docutils literal notranslate"><span class="pre">addAlt</span></code> and <code class="docutils literal notranslate"><span class="pre">addAlt'</span></code> below are essentially the
same; the only difference is that we use anonymous constructor notation
in the second.
Although it is sometimes convenient to define functions this way, and structural eta-reduction makes
this alternative definitionally equivalent, it can make things less convenient in later proofs.
In particular, <code class="docutils literal notranslate"><span class="pre">rw</span> <span class="pre">[addAlt]</span></code> leaves us with a messier goal view containing a <code class="docutils literal notranslate"><span class="pre">match</span></code> statement.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">addAlt</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Point</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">Point.mk</span><span class="w"> </span><span class="n">x&#8321;</span><span class="w"> </span><span class="n">y&#8321;</span><span class="w"> </span><span class="n">z&#8321;</span><span class="o">,</span><span class="w"> </span><span class="n">Point.mk</span><span class="w"> </span><span class="n">x&#8322;</span><span class="w"> </span><span class="n">y&#8322;</span><span class="w"> </span><span class="n">z&#8322;</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">x&#8321;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x&#8322;</span><span class="o">,</span><span class="w"> </span><span class="n">y&#8321;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y&#8322;</span><span class="o">,</span><span class="w"> </span><span class="n">z&#8321;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">z&#8322;</span><span class="o">&#10217;</span>

<span class="kd">def</span><span class="w"> </span><span class="n">addAlt&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Point</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">x&#8321;</span><span class="o">,</span><span class="w"> </span><span class="n">y&#8321;</span><span class="o">,</span><span class="w"> </span><span class="n">z&#8321;</span><span class="o">&#10217;,</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">x&#8322;</span><span class="o">,</span><span class="w"> </span><span class="n">y&#8322;</span><span class="o">,</span><span class="w"> </span><span class="n">z&#8322;</span><span class="o">&#10217;</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">x&#8321;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x&#8322;</span><span class="o">,</span><span class="w"> </span><span class="n">y&#8321;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y&#8322;</span><span class="o">,</span><span class="w"> </span><span class="n">z&#8321;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">z&#8322;</span><span class="o">&#10217;</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">addAlt_x</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a.addAlt</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="bp">.</span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a.x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">addAlt_comm</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">addAlt</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">addAlt</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">addAlt</span><span class="o">,</span><span class="w"> </span><span class="n">addAlt</span><span class="o">]</span>
<span class="w">  </span><span class="c1">-- the same proof still works, but the goal view here is harder to read</span>
<span class="w">  </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">dsimp</span>
<span class="w">  </span><span class="n">repeat&#39;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">add_comm</span>
</pre></div>
</div>
<p>Mathematical constructions often involve taking apart bundled information and
putting it together again in different ways.
It therefore makes sense that Lean and Mathlib offer so many ways
of doing this efficiently.
As an exercise, try proving that <code class="docutils literal notranslate"><span class="pre">Point.add</span></code> is associative.
Then define scalar multiplication for a point and show that it
distributes over addition.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">protected</span><span class="w"> </span><span class="kd">theorem</span><span class="w"> </span><span class="n">add_assoc</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a.add</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="bp">.</span><span class="n">add</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a.add</span><span class="w"> </span><span class="o">(</span><span class="n">b.add</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">def</span><span class="w"> </span><span class="n">smul</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">smul_distrib</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">smul</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="bp">.</span><span class="n">add</span><span class="w"> </span><span class="o">(</span><span class="n">smul</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">smul</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="o">(</span><span class="n">a.add</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Using structures is only the first step on the road to
algebraic abstraction.
We don&#8217;t yet have a way to link <code class="docutils literal notranslate"><span class="pre">Point.add</span></code> to the generic <code class="docutils literal notranslate"><span class="pre">+</span></code> symbol,
or to connect <code class="docutils literal notranslate"><span class="pre">Point.add_comm</span></code> and <code class="docutils literal notranslate"><span class="pre">Point.add_assoc</span></code> to
the generic <code class="docutils literal notranslate"><span class="pre">add_comm</span></code> and <code class="docutils literal notranslate"><span class="pre">add_assoc</span></code> theorems.
These tasks belong to the <em>algebraic</em> aspect of using structures,
and we will explain how to carry them out in the next section.
For now, just think of a structure as a way of bundling together objects
and information.</p>
<p>It is especially useful that a structure can specify not only
data types but also constraints that the data must satisfy.
In Lean, the latter are represented as fields of type <code class="docutils literal notranslate"><span class="pre">Prop</span></code>.
For example, the <em>standard 2-simplex</em> is defined to be the set of
points <span class="math notranslate nohighlight">\((x, y, z)\)</span> satisfying <span class="math notranslate nohighlight">\(x &#8805; 0\)</span>, <span class="math notranslate nohighlight">\(y &#8805; 0\)</span>, <span class="math notranslate nohighlight">\(z &#8805; 0\)</span>,
and <span class="math notranslate nohighlight">\(x + y + z = 1\)</span>.
If you are not familiar with the notion, you should draw a picture,
and convince yourself that this set is
the equilateral triangle in three-space with vertices
<span class="math notranslate nohighlight">\((1, 0, 0)\)</span>, <span class="math notranslate nohighlight">\((0, 1, 0)\)</span>, and <span class="math notranslate nohighlight">\((0, 0, 1)\)</span>,
together with its interior.
We can represent it in Lean as follows:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">structure</span><span class="w"> </span><span class="n">StandardTwoSimplex</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">x_nonneg</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">y_nonneg</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">y</span>
<span class="w">  </span><span class="n">z_nonneg</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">z</span>
<span class="w">  </span><span class="n">sum_eq</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span>
</pre></div>
</div>
<p>Notice that the last four fields refer to <code class="docutils literal notranslate"><span class="pre">x</span></code>, <code class="docutils literal notranslate"><span class="pre">y</span></code>, and <code class="docutils literal notranslate"><span class="pre">z</span></code>,
that is, the first three fields.
We can define a map from the two-simplex to itself that swaps <code class="docutils literal notranslate"><span class="pre">x</span></code> and <code class="docutils literal notranslate"><span class="pre">y</span></code>:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">swapXy</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StandardTwoSimplex</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StandardTwoSimplex</span>
<span class="w">    </span><span class="n">where</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.y</span>
<span class="w">  </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.x</span>
<span class="w">  </span><span class="n">z</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.z</span>
<span class="w">  </span><span class="n">x_nonneg</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.y_nonneg</span>
<span class="w">  </span><span class="n">y_nonneg</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.x_nonneg</span>
<span class="w">  </span><span class="n">z_nonneg</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">a.z_nonneg</span>
<span class="w">  </span><span class="n">sum_eq</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add_comm</span><span class="w"> </span><span class="n">a.y</span><span class="w"> </span><span class="n">a.x</span><span class="o">,</span><span class="w"> </span><span class="n">a.sum_eq</span><span class="o">]</span>
</pre></div>
</div>
<p>More interestingly, we can compute the midpoint of two points on
the simplex. We have added the phrase <code class="docutils literal notranslate"><span class="pre">noncomputable</span> <span class="pre">section</span></code>
at the beginning of this file in order to use division on the real numbers.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">noncomputable</span><span class="w"> </span><span class="kn">section</span>

<span class="kd">def</span><span class="w"> </span><span class="n">midpoint</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StandardTwoSimplex</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StandardTwoSimplex</span>
<span class="w">    </span><span class="n">where</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">a.x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.x</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span>
<span class="w">  </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">a.y</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.y</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span>
<span class="w">  </span><span class="n">z</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">a.z</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.z</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span>
<span class="w">  </span><span class="n">x_nonneg</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">div_nonneg</span><span class="w"> </span><span class="o">(</span><span class="n">add_nonneg</span><span class="w"> </span><span class="n">a.x_nonneg</span><span class="w"> </span><span class="n">b.x_nonneg</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span><span class="o">)</span>
<span class="w">  </span><span class="n">y_nonneg</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">div_nonneg</span><span class="w"> </span><span class="o">(</span><span class="n">add_nonneg</span><span class="w"> </span><span class="n">a.y_nonneg</span><span class="w"> </span><span class="n">b.y_nonneg</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span><span class="o">)</span>
<span class="w">  </span><span class="n">z_nonneg</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">div_nonneg</span><span class="w"> </span><span class="o">(</span><span class="n">add_nonneg</span><span class="w"> </span><span class="n">a.z_nonneg</span><span class="w"> </span><span class="n">b.z_nonneg</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span><span class="o">)</span>
<span class="w">  </span><span class="n">sum_eq</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">field_simp</span><span class="bp">;</span><span class="w"> </span><span class="n">linarith</span><span class="w"> </span><span class="o">[</span><span class="n">a.sum_eq</span><span class="o">,</span><span class="w"> </span><span class="n">b.sum_eq</span><span class="o">]</span>
</pre></div>
</div>
<p>Here we have established <code class="docutils literal notranslate"><span class="pre">x_nonneg</span></code>, <code class="docutils literal notranslate"><span class="pre">y_nonneg</span></code>, and <code class="docutils literal notranslate"><span class="pre">z_nonneg</span></code>
with concise proof terms, but establish <code class="docutils literal notranslate"><span class="pre">sum_eq</span></code> in tactic mode,
using <code class="docutils literal notranslate"><span class="pre">by</span></code>.</p>
<p>Given a parameter <span class="math notranslate nohighlight">\(\lambda\)</span> satisfying <span class="math notranslate nohighlight">\(0 \le \lambda \le 1\)</span>,
we can take the weighted average <span class="math notranslate nohighlight">\(\lambda a + (1 - \lambda) b\)</span>
of two points <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> in the standard 2-simplex.
We challenge you to define that function, in analogy to the <code class="docutils literal notranslate"><span class="pre">midpoint</span></code>
function above.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">weightedAverage</span><span class="w"> </span><span class="o">(</span><span class="n">lambda</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Real</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">lambda_nonneg</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">lambda</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">lambda_le</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">lambda</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StandardTwoSimplex</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StandardTwoSimplex</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Structures can depend on parameters.
For example, we can generalize the standard 2-simplex to the standard
<span class="math notranslate nohighlight">\(n\)</span>-simplex for any <span class="math notranslate nohighlight">\(n\)</span>.
At this stage, you don&#8217;t have to know anything about the type <code class="docutils literal notranslate"><span class="pre">Fin</span> <span class="pre">n</span></code>
except that it has <span class="math notranslate nohighlight">\(n\)</span> elements, and that Lean knows
how to sum over it.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">BigOperators</span>

<span class="kd">structure</span><span class="w"> </span><span class="n">StandardSimplex</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">V</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">NonNeg</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span>
<span class="w">  </span><span class="n">sum_eq_one</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span>

<span class="kn">namespace</span><span class="w"> </span><span class="n">StandardSimplex</span>

<span class="kd">def</span><span class="w"> </span><span class="n">midpoint</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StandardSimplex</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StandardSimplex</span><span class="w"> </span><span class="n">n</span>
<span class="w">    </span><span class="n">where</span>
<span class="w">  </span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">a.V</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.V</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span>
<span class="w">  </span><span class="n">NonNeg</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span><span class="w"> </span><span class="n">i</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">div_nonneg</span>
<span class="w">    </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">linarith</span><span class="w"> </span><span class="o">[</span><span class="n">a.NonNeg</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">b.NonNeg</span><span class="w"> </span><span class="n">i</span><span class="o">]</span>
<span class="w">    </span><span class="n">norm_num</span>
<span class="w">  </span><span class="n">sum_eq_one</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">div_eq_mul_inv</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">Finset.sum_mul</span><span class="o">,</span><span class="w"> </span><span class="n">Finset.sum_add_distrib</span><span class="o">,</span>
<span class="w">      </span><span class="n">a.sum_eq_one</span><span class="o">,</span><span class="w"> </span><span class="n">b.sum_eq_one</span><span class="o">]</span>
<span class="w">    </span><span class="n">field_simp</span>

<span class="kd">end</span><span class="w"> </span><span class="n">StandardSimplex</span>
</pre></div>
</div>
<p>As an exercise, see if you can define the weighted average of
two points in the standard <span class="math notranslate nohighlight">\(n\)</span>-simplex.
You can use <code class="docutils literal notranslate"><span class="pre">Finset.sum_add_distrib</span></code>
and <code class="docutils literal notranslate"><span class="pre">Finset.mul_sum</span></code> to manipulate the relevant sums.</p>
<p>We have seen that structures can be used to bundle together data
and properties.
Interestingly, they can also be used to bundle together properties
without the data.
For example, the next structure, <code class="docutils literal notranslate"><span class="pre">IsLinear</span></code>, bundles together
the two components of linearity.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">structure</span><span class="w"> </span><span class="n">IsLinear</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">is_additive</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">y</span>
<span class="w">  </span><span class="n">preserves_mul</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">c</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span>

<span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">linf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsLinear</span><span class="w"> </span><span class="n">f</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">linf.is_additive</span>
<span class="k">#check</span><span class="w"> </span><span class="n">linf.preserves_mul</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>It is worth pointing out that structures are not the only way to bundle
together data.
The <code class="docutils literal notranslate"><span class="pre">Point</span></code> data structure can be defined using the generic type product,
and <code class="docutils literal notranslate"><span class="pre">IsLinear</span></code> can be defined with a simple <code class="docutils literal notranslate"><span class="pre">and</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">Point&#39;&#39;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">&#8477;</span>

<span class="kd">def</span><span class="w"> </span><span class="n">IsLinear&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">(</span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">c</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span>
</pre></div>
</div>
<p>Generic type constructions can even be used in place of structures
with dependencies between their components.
For example, the <em>subtype</em> construction combines a piece of data with
a property.
You can think of the type <code class="docutils literal notranslate"><span class="pre">PReal</span></code> in the next example as being
the type of positive real numbers.
Any <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">:</span> <span class="pre">PReal</span></code> has two components: the value, and the property of being
positive.
You can access these components as <code class="docutils literal notranslate"><span class="pre">x.val</span></code>, which has type <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>,
and <code class="docutils literal notranslate"><span class="pre">x.property</span></code>, which represents the fact <code class="docutils literal notranslate"><span class="pre">0</span> <span class="pre">&lt;</span> <span class="pre">x.val</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">PReal</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">{</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">//</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">}</span>

<span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">PReal</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">x.val</span>
<span class="k">#check</span><span class="w"> </span><span class="n">x.property</span>
<span class="k">#check</span><span class="w"> </span><span class="n">x</span><span class="bp">.</span><span class="mi">1</span>
<span class="k">#check</span><span class="w"> </span><span class="n">x</span><span class="bp">.</span><span class="mi">2</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>We could have used subtypes to define the standard 2-simplex,
as well as the standard <span class="math notranslate nohighlight">\(n\)</span>-simplex for an arbitrary <span class="math notranslate nohighlight">\(n\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">StandardTwoSimplex&#39;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">{</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">//</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">p</span><span class="bp">.</span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">p</span><span class="bp">.</span><span class="mi">2</span><span class="bp">.</span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">p</span><span class="bp">.</span><span class="mi">2</span><span class="bp">.</span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">p</span><span class="bp">.</span><span class="mi">1</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">p</span><span class="bp">.</span><span class="mi">2</span><span class="bp">.</span><span class="mi">1</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">p</span><span class="bp">.</span><span class="mi">2</span><span class="bp">.</span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">}</span>

<span class="kd">def</span><span class="w"> </span><span class="n">StandardSimplex&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">{</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">//</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">}</span>
</pre></div>
</div>
<p>Similarly, <em>Sigma types</em> are generalizations of ordered pairs,
whereby the type of the second component depends on the type of
the first.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">StdSimplex</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="bp">&#931;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="n">StandardSimplex</span><span class="w"> </span><span class="n">n</span>

<span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">StdSimplex</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">s.fst</span>
<span class="k">#check</span><span class="w"> </span><span class="n">s.snd</span>

<span class="k">#check</span><span class="w"> </span><span class="n">s</span><span class="bp">.</span><span class="mi">1</span>
<span class="k">#check</span><span class="w"> </span><span class="n">s</span><span class="bp">.</span><span class="mi">2</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>Given <code class="docutils literal notranslate"><span class="pre">s</span> <span class="pre">:</span> <span class="pre">StdSimplex</span></code>, the first component <code class="docutils literal notranslate"><span class="pre">s.fst</span></code> is a natural
number, and the second component is an element of the corresponding
simplex <code class="docutils literal notranslate"><span class="pre">StandardSimplex</span> <span class="pre">s.fst</span></code>.
The difference between a Sigma type and a subtype is that
the second component of a Sigma type is data rather than a proposition.</p>
<p>But even though we can use products, subtypes, and Sigma types
instead of structures, using structures has a number of advantages.
Defining a structure abstracts away the underlying representation
and provides custom names for the functions that access the components.
This makes proofs more robust:
proofs that rely only on the interface to a structure
will generally continue to work when we change the definition,
as long as we redefine the old accessors in terms of the new definition.
Moreover, as we are about to see, Lean provides support for
weaving structures together into a rich, interconnected hierarchy,
and for managing the interactions between them.</p>
</section>
<section id="algebraic-structures">
<span id="section-algebraic-structures"></span><h2><span class="section-number">7.2. </span>Algebraic Structures<a class="headerlink" href="#algebraic-structures" title="Link to this heading">&#61633;</a></h2>
<p>To clarify what we mean by the phrase <em>algebraic structure</em>,
it will help to consider some examples.</p>
<ol class="arabic simple">
<li><p>A <em>partially ordered set</em> consists of a set <span class="math notranslate nohighlight">\(P\)</span> and
a binary relation <span class="math notranslate nohighlight">\(\le\)</span> on <span class="math notranslate nohighlight">\(P\)</span> that is transitive
and reflexive.</p></li>
<li><p>A <em>group</em> consists of a set <span class="math notranslate nohighlight">\(G\)</span> with an associative
binary operation, an identity element
<span class="math notranslate nohighlight">\(1\)</span>, and a function <span class="math notranslate nohighlight">\(g \mapsto g^{-1}\)</span> that returns
an inverse for each <span class="math notranslate nohighlight">\(g\)</span> in <span class="math notranslate nohighlight">\(G\)</span>.
A group is <em>abelian</em> or <em>commutative</em> if the operation is commutative.</p></li>
<li><p>A <em>lattice</em> is a partially ordered set with meets and joins.</p></li>
<li><p>A <em>ring</em> consists of an (additively written) abelian group
<span class="math notranslate nohighlight">\((R, +, 0, x \mapsto -x)\)</span>
together with an associative multiplication operation
<span class="math notranslate nohighlight">\(\cdot\)</span> and an identity <span class="math notranslate nohighlight">\(1\)</span>,
such that multiplication distributes over addition.
A ring is <em>commutative</em> if the multiplication is commutative.</p></li>
<li><p>An <em>ordered ring</em> <span class="math notranslate nohighlight">\((R, +, 0, -, \cdot, 1, \le)\)</span> consists of a ring
together with a partial order on its elements, such that <span class="math notranslate nohighlight">\(a \le b\)</span> implies
<span class="math notranslate nohighlight">\(a + c \le b + c\)</span> for every <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span>, and <span class="math notranslate nohighlight">\(c\)</span> in <span class="math notranslate nohighlight">\(R\)</span>,
and <span class="math notranslate nohighlight">\(0 \le a\)</span> and <span class="math notranslate nohighlight">\(0 \le b\)</span> implies <span class="math notranslate nohighlight">\(0 \le a b\)</span> for
every <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> in <span class="math notranslate nohighlight">\(R\)</span>.</p></li>
<li><p>A <em>metric space</em> consists of a set <span class="math notranslate nohighlight">\(X\)</span> and a function
<span class="math notranslate nohighlight">\(d : X \times X \to \mathbb{R}\)</span> such that the following hold:</p>
<ul class="simple">
<li><p><span class="math notranslate nohighlight">\(d(x, y) \ge 0\)</span> for every <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> in <span class="math notranslate nohighlight">\(X\)</span>.</p></li>
<li><p><span class="math notranslate nohighlight">\(d(x, y) = 0\)</span> if and only if <span class="math notranslate nohighlight">\(x = y\)</span>.</p></li>
<li><p><span class="math notranslate nohighlight">\(d(x, y) = d(y, x)\)</span> for every <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> in <span class="math notranslate nohighlight">\(X\)</span>.</p></li>
<li><p><span class="math notranslate nohighlight">\(d(x, z) \le d(x, y) + d(y, z)\)</span> for every <span class="math notranslate nohighlight">\(x\)</span>, <span class="math notranslate nohighlight">\(y\)</span>, and
<span class="math notranslate nohighlight">\(z\)</span> in <span class="math notranslate nohighlight">\(X\)</span>.</p></li>
</ul>
</li>
<li><p>A <em>topological space</em> consists of a set <span class="math notranslate nohighlight">\(X\)</span> and a collection <span class="math notranslate nohighlight">\(\mathcal T\)</span>
of subsets of <span class="math notranslate nohighlight">\(X\)</span>, called the <em>open subsets of</em> <span class="math notranslate nohighlight">\(X\)</span>, such that
the following hold:</p>
<ul class="simple">
<li><p>The empty set and <span class="math notranslate nohighlight">\(X\)</span> are open.</p></li>
<li><p>The intersection of two open sets is open.</p></li>
<li><p>An arbitrary union of open sets is open.</p></li>
</ul>
</li>
</ol>
<p>In each of these examples, the elements of the structure belong to a
set, the <em>carrier set</em>,
that sometimes stands proxy for the entire structure.
For example, when we say &#8220;let <span class="math notranslate nohighlight">\(G\)</span> be a group&#8221; and then
&#8220;let <span class="math notranslate nohighlight">\(g \in G\)</span>,&#8221; we are using <span class="math notranslate nohighlight">\(G\)</span> to stand for both
the structure and its carrier.
Not every algebraic structure is associated with a single carrier set in this way.
For example, a <em>bipartite graph</em> involves a relation between two sets,
as does a <em>Galois connection</em>,
A <em>category</em> also involves two sets of interest, commonly called the <em>objects</em>
and the <em>morphisms</em>.</p>
<p>The examples indicate some of the things that a proof assistant has to do
in order to support algebraic reasoning.
First, it needs to recognize concrete instances of structures.
The number systems <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span>, <span class="math notranslate nohighlight">\(\mathbb{Q}\)</span>,
and <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> are all ordered rings,
and we should be able to apply a generic theorem about ordered rings
in any of these instances.
Sometimes a concrete set may be an instance of a structure in more than one way.
For example, in addition to the usual topology on <span class="math notranslate nohighlight">\(\mathbb{R}\)</span>,
which forms the basis for real analysis,
we can also consider the <em>discrete</em> topology on <span class="math notranslate nohighlight">\(\mathbb{R}\)</span>,
in which every set is open.</p>
<p>Second, a proof assistant needs to support generic notation on structures.
In Lean, the notation <code class="docutils literal notranslate"><span class="pre">*</span></code>
is used for multiplication in all the usual number systems,
as well as for multiplication in generic groups and rings.
When we use an expression like <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">x</span> <span class="pre">*</span> <span class="pre">y</span></code>,
Lean has to use information about the types of <code class="docutils literal notranslate"><span class="pre">f</span></code>, <code class="docutils literal notranslate"><span class="pre">x</span></code>, and <code class="docutils literal notranslate"><span class="pre">y</span></code>
to determine which multiplication we have in mind.</p>
<p>Third, it needs to deal with the fact that structures can inherit
definitions, theorems, and notation from other structures in various ways.
Some structures extend others by adding more axioms.
A commutative ring is still a ring, so any definition
that makes sense in a ring also makes sense in a commutative ring,
and any theorem that holds in a ring also holds in a commutative ring.
Some structures extend others by adding more data.
For example, the additive part of any ring is an additive group.
The ring structure adds a multiplication and an identity,
as well as axioms that govern them and relate them to the additive part.
Sometimes we can define one structure in terms of another.
Any metric space has a canonical topology associated with it,
the <em>metric space topology</em>, and there are various topologies that can be
associated with any linear ordering.</p>
<p>Finally, it is important to keep in mind that mathematics allows us to
use functions and operations to define structures in the same way we
use functions and operations to define numbers.
Products and powers of groups are again groups.
For every <span class="math notranslate nohighlight">\(n\)</span>, the integers modulo <span class="math notranslate nohighlight">\(n\)</span> form a ring,
and for every <span class="math notranslate nohighlight">\(k &gt; 0\)</span>, the <span class="math notranslate nohighlight">\(k \times k\)</span> matrices of polynomials
with coefficients in that ring again form a ring.
Thus we can calculate with structures just as easily as we can calculate
with their elements.
This means that algebraic structures lead dual lives in mathematics,
as containers for collections of objects and as objects in their own right.
A proof assistant has to accommodate this dual role.</p>
<p>When dealing with elements of a type that has an algebraic structure
associated with it,
a proof assistant needs to recognize the structure and find the relevant
definitions, theorems, and notation.
All this should sound like a lot of work, and it is.
But Lean uses a small collection of fundamental mechanisms to
carry out these tasks.
The goal of this section is to explain these mechanisms and show you
how to use them.</p>
<p>The first ingredient is almost too obvious to mention:
formally speaking, algebraic structures are structures in the sense
of <a class="reference internal" href="#section-structures"><span class="std std-numref">Section 7.1</span></a>.
An algebraic structure is a specification of a bundle of data satisfying
some axiomatic hypotheses, and we saw in <a class="reference internal" href="#section-structures"><span class="std std-numref">Section 7.1</span></a> that
this is exactly what the <code class="docutils literal notranslate"><span class="pre">structure</span></code> command is designed to accommodate.
It&#8217;s a marriage made in heaven!</p>
<p>Given a data type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>, we can define the group structure on <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>
as follows.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">structure</span><span class="w"> </span><span class="n">Group&#8321;</span><span class="w"> </span><span class="o">(</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">mul</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="n">one</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="n">inv</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="n">mul_assoc</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="o">(</span><span class="n">mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">(</span><span class="n">mul</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="o">)</span>
<span class="w">  </span><span class="n">mul_one</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">one</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">one_mul</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">one</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">inv_mul_cancel</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="o">(</span><span class="n">inv</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">one</span>
</pre></div>
</div>
<p>Notice that the type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> is a <em>parameter</em> in the definition of <code class="docutils literal notranslate"><span class="pre">Group&#8321;</span></code>.
So you should think of an object <code class="docutils literal notranslate"><span class="pre">struc</span> <span class="pre">:</span> <span class="pre">Group&#8321;</span> <span class="pre">&#945;</span></code> as being
a group structure on <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>.
We saw in <a class="reference internal" href="C02_Basics.html#proving-identities-in-algebraic-structures"><span class="std std-numref">Section 2.2</span></a>
that the counterpart <code class="docutils literal notranslate"><span class="pre">mul_inv_cancel</span></code> to <code class="docutils literal notranslate"><span class="pre">inv_mul_cancel</span></code>
follows from the other group axioms, so there is no need
to add it to the definition.</p>
<p>This definition of a group is similar to the definition of <code class="docutils literal notranslate"><span class="pre">Group</span></code> in
Mathlib,
and we have chosen the name <code class="docutils literal notranslate"><span class="pre">Group&#8321;</span></code> to distinguish our version.
If you write <code class="docutils literal notranslate"><span class="pre">#check</span> <span class="pre">Group</span></code> and ctrl-click on the definition,
you will see that the Mathlib version of <code class="docutils literal notranslate"><span class="pre">Group</span></code> is defined to
extend another structure; we will explain how to do that later.
If you type <code class="docutils literal notranslate"><span class="pre">#print</span> <span class="pre">Group</span></code> you will also see that the Mathlib
version of <code class="docutils literal notranslate"><span class="pre">Group</span></code> has a number of extra fields.
For reasons we will explain later, sometimes it is useful to add
redundant information to a structure,
so that there are additional fields for objects and functions
that can be defined from the core
data. Don&#8217;t worry about that for now.
Rest assured that our simplified version <code class="docutils literal notranslate"><span class="pre">Group&#8321;</span></code> is
morally the same as the definition of a group that Mathlib uses.</p>
<p>It is sometimes useful to bundle
the type together with the structure, and Mathlib also
contains a definition of a <code class="docutils literal notranslate"><span class="pre">Grp</span></code> structure that is equivalent to
the following:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">structure</span><span class="w"> </span><span class="n">Grp&#8321;</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span>
<span class="w">  </span><span class="n">str</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Group&#8321;</span><span class="w"> </span><span class="n">&#945;</span>
</pre></div>
</div>
<p>The Mathlib version is found in <code class="docutils literal notranslate"><span class="pre">Mathlib.Algebra.Category.Grp.Basic</span></code>,
and you can <code class="docutils literal notranslate"><span class="pre">#check</span></code> it if you add this to the imports at the
beginning of the examples file.</p>
<p>For reasons that will become clearer below, it is more often
useful to keep the type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> separate from the structure <code class="docutils literal notranslate"><span class="pre">Group</span> <span class="pre">&#945;</span></code>.
We refer to the two objects together as a <em>partially bundled structure</em>,
since the representation combines most, but not all, of the components
into one structure. It is common in Mathlib
to use capital roman letters like <code class="docutils literal notranslate"><span class="pre">G</span></code> for a type
when it is used as the carrier type for a group.</p>
<p>Let&#8217;s construct a group, which is to say, an element of the <code class="docutils literal notranslate"><span class="pre">Group&#8321;</span></code> type.
For any pair of types <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#946;</span></code>, Mathlib defines the type <code class="docutils literal notranslate"><span class="pre">Equiv</span> <span class="pre">&#945;</span> <span class="pre">&#946;</span></code>
of <em>equivalences</em> between <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#946;</span></code>.
Mathlib also defines the suggestive notation <code class="docutils literal notranslate"><span class="pre">&#945;</span> <span class="pre">&#8771;</span> <span class="pre">&#946;</span></code> for this type.
An element <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">&#945;</span> <span class="pre">&#8771;</span> <span class="pre">&#946;</span></code> is a bijection between <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#946;</span></code>
represented by four components:
a function <code class="docutils literal notranslate"><span class="pre">f.toFun</span></code> from <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> to <code class="docutils literal notranslate"><span class="pre">&#946;</span></code>,
the inverse function <code class="docutils literal notranslate"><span class="pre">f.invFun</span></code> from <code class="docutils literal notranslate"><span class="pre">&#946;</span></code> to <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>,
and two properties that specify these functions are indeed inverse
to one another.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">&#945;</span><span class="w"> </span><span class="n">&#946;</span><span class="w"> </span><span class="n">&#947;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="n">&#946;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#946;</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="n">&#947;</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Equiv</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="n">&#946;</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">f.toFun</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#946;</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">f.invFun</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#946;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">f.right_inv</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#946;</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">f.invFun</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">f.left_inv</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">f.invFun</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">Equiv.refl</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">f.symm</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#946;</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">f.trans</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="n">&#947;</span><span class="o">)</span>
</pre></div>
</div>
<p>Notice the creative naming of the last three constructions. We think of the
identity function <code class="docutils literal notranslate"><span class="pre">Equiv.refl</span></code>, the inverse operation <code class="docutils literal notranslate"><span class="pre">Equiv.symm</span></code>,
and the composition operation <code class="docutils literal notranslate"><span class="pre">Equiv.trans</span></code> as explicit evidence
that the property of being in bijective correspondence is an equivalence relation.</p>
<p>Notice also that <code class="docutils literal notranslate"><span class="pre">f.trans</span> <span class="pre">g</span></code> requires composing the forward functions
in reverse order. Mathlib has declared a <em>coercion</em> from <code class="docutils literal notranslate"><span class="pre">Equiv</span> <span class="pre">&#945;</span> <span class="pre">&#946;</span></code>
to the function type <code class="docutils literal notranslate"><span class="pre">&#945;</span> <span class="pre">&#8594;</span> <span class="pre">&#946;</span></code>, so we can omit writing <code class="docutils literal notranslate"><span class="pre">.toFun</span></code>
and have Lean insert it for us.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">f.trans</span><span class="w"> </span><span class="n">g</span><span class="o">)</span><span class="bp">.</span><span class="n">toFun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">g.toFun</span><span class="w"> </span><span class="o">(</span><span class="n">f.toFun</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">f.trans</span><span class="w"> </span><span class="n">g</span><span class="o">)</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">f.trans</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#947;</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">&#8728;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>Mathlib also defines the type <code class="docutils literal notranslate"><span class="pre">perm</span> <span class="pre">&#945;</span></code> of equivalences between
<code class="docutils literal notranslate"><span class="pre">&#945;</span></code> and itself.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Equiv.Perm</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>It should be clear that <code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">&#945;</span></code> forms a group under composition
of equivalences. We orient things so that <code class="docutils literal notranslate"><span class="pre">mul</span> <span class="pre">f</span> <span class="pre">g</span></code> is
equal to <code class="docutils literal notranslate"><span class="pre">g.trans</span> <span class="pre">f</span></code>, whose forward function is <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">&#8728;</span> <span class="pre">g</span></code>.
In other words, multiplication is what we ordinarily think of as
composition of the bijections. Here we define this group:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">permGroup</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Group&#8321;</span><span class="w"> </span><span class="o">(</span><span class="n">Equiv.Perm</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>
<span class="w">    </span><span class="n">where</span>
<span class="w">  </span><span class="n">mul</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.trans</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">f</span>
<span class="w">  </span><span class="n">one</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.refl</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="n">inv</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.symm</span>
<span class="w">  </span><span class="n">mul_assoc</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">Equiv.trans_assoc</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="o">)</span><span class="bp">.</span><span class="n">symm</span>
<span class="w">  </span><span class="n">one_mul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.trans_refl</span>
<span class="w">  </span><span class="n">mul_one</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.refl_trans</span>
<span class="w">  </span><span class="n">inv_mul_cancel</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.self_trans_symm</span>
</pre></div>
</div>
<p>In fact, Mathlib defines exactly this <code class="docutils literal notranslate"><span class="pre">Group</span></code> structure on <code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">&#945;</span></code>
in the file <code class="docutils literal notranslate"><span class="pre">Algebra.Group.End</span></code>.
As always, you can hover over the theorems used in the definition of
<code class="docutils literal notranslate"><span class="pre">permGroup</span></code> to see their statements,
and you can jump to their definitions in the original file to learn
more about how they are implemented.</p>
<p>In ordinary mathematics, we generally think of notation as
independent of structure.
For example, we can consider groups <span class="math notranslate nohighlight">\((G_1, \cdot, 1, \cdot^{-1})\)</span>,
<span class="math notranslate nohighlight">\((G_2, \circ, e, i(\cdot))\)</span>, and <span class="math notranslate nohighlight">\((G_3, +, 0, -)\)</span>.
In the first case, we write the binary operation as <span class="math notranslate nohighlight">\(\cdot\)</span>,
the identity as <span class="math notranslate nohighlight">\(1\)</span>, and the inverse function as <span class="math notranslate nohighlight">\(x \mapsto x^{-1}\)</span>.
In the second and third cases, we use the notational alternatives shown.
When we formalize the notion of a group in Lean, however,
the notation is more tightly linked to the structure.
In Lean, the components of any <code class="docutils literal notranslate"><span class="pre">Group</span></code> are named
<code class="docutils literal notranslate"><span class="pre">mul</span></code>, <code class="docutils literal notranslate"><span class="pre">one</span></code>, and <code class="docutils literal notranslate"><span class="pre">inv</span></code>,
and in a moment we will see how multiplicative notation is
set up to refer to them.
If we want to use additive notation, we instead use an isomorphic structure
<code class="docutils literal notranslate"><span class="pre">AddGroup</span></code> (the structure underlying additive groups). Its components are named <code class="docutils literal notranslate"><span class="pre">add</span></code>, <code class="docutils literal notranslate"><span class="pre">zero</span></code>,
and <code class="docutils literal notranslate"><span class="pre">neg</span></code>, and the associated notation is what you would expect it to be.</p>
<p>Recall the type <code class="docutils literal notranslate"><span class="pre">Point</span></code> that we defined in <a class="reference internal" href="#section-structures"><span class="std std-numref">Section 7.1</span></a>,
and the addition function that we defined there.
These definitions are reproduced in the examples file that accompanies
this section.
As an exercise, define an <code class="docutils literal notranslate"><span class="pre">AddGroup&#8321;</span></code> structure that is similar
to the <code class="docutils literal notranslate"><span class="pre">Group&#8321;</span></code> structure we defined above, except that it uses the
additive naming scheme just described.
Define negation and a zero on the <code class="docutils literal notranslate"><span class="pre">Point</span></code> data type,
and define the <code class="docutils literal notranslate"><span class="pre">AddGroup&#8321;</span></code> structure on <code class="docutils literal notranslate"><span class="pre">Point</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">structure</span><span class="w"> </span><span class="n">AddGroup&#8321;</span><span class="w"> </span><span class="o">(</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="o">(</span><span class="n">add</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>
<span class="w">  </span><span class="c1">-- fill in the rest</span>
<span class="kd">@[</span><span class="n">ext</span><span class="kd">]</span>
<span class="kd">structure</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>
<span class="w">  </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span>

<span class="kn">namespace</span><span class="w"> </span><span class="n">Point</span>

<span class="kd">def</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="n">a.x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.x</span><span class="o">,</span><span class="w"> </span><span class="n">a.y</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.y</span><span class="o">,</span><span class="w"> </span><span class="n">a.z</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b.z</span><span class="o">&#10217;</span>

<span class="kd">def</span><span class="w"> </span><span class="n">neg</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>

<span class="kd">def</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>

<span class="kd">def</span><span class="w"> </span><span class="n">addGroupPoint</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">AddGroup&#8321;</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>

<span class="kd">end</span><span class="w"> </span><span class="n">Point</span>
</pre></div>
</div>
<p>We are making progress.
Now we know how to define algebraic structures in Lean,
and we know how to define instances of those structures.
But we also want to associate notation with structures
so that we can use it with each instance.
Moreover, we want to arrange it so that we can define an operation
on a structure and use it with any particular instance,
and we want to arrange it so that we can prove a theorem about
a structure and use it with any instance.</p>
<p>In fact, Mathlib is already set up to use generic group notation,
definitions, and theorems for <code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">&#945;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Equiv.Perm</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g</span>
<span class="k">#check</span><span class="w"> </span><span class="n">mul_assoc</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">g</span><span class="bp">&#8315;&#185;</span>

<span class="c1">-- group power, defined for any group</span>
<span class="k">#check</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">n</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mul_assoc</span><span class="o">,</span><span class="w"> </span><span class="n">mul_inv_cancel</span><span class="o">,</span><span class="w"> </span><span class="n">mul_one</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">mul_inv_cancel_right</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Equiv.Perm</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">g.symm.trans</span><span class="w"> </span><span class="o">(</span><span class="n">g.trans</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">mul_inv_cancel_right</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span>
</pre></div>
</div>
<p>You can check that this is not the case for the additive group structure
on <code class="docutils literal notranslate"><span class="pre">Point</span></code> that we asked you to define above.
Our task now is to understand that magic that goes on under the hood
in order to make the examples for <code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">&#945;</span></code> work the way they do.</p>
<p>The issue is that Lean needs to be able to <em>find</em> the relevant
notation and the implicit group structure,
using the information that is found in the expressions that we type.
Similarly, when we write <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">+</span> <span class="pre">y</span></code> with expressions <code class="docutils literal notranslate"><span class="pre">x</span></code> and <code class="docutils literal notranslate"><span class="pre">y</span></code>
that have type <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>, Lean needs to interpret the <code class="docutils literal notranslate"><span class="pre">+</span></code>
symbol as the relevant addition function on the reals.
It also has to recognize the type <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> as an instance of a commutative ring,
so that all the definitions and theorems for a commutative ring are available.
For another example,
continuity is defined in Lean relative to any two topological spaces.
When we have <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">&#8450;</span></code> and we write <code class="docutils literal notranslate"><span class="pre">Continuous</span> <span class="pre">f</span></code>, Lean has to find the
relevant topologies on <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#8450;</span></code>.</p>
<p>The magic is achieved with a combination of three things.</p>
<ol class="arabic simple">
<li><p><em>Logic.</em> A definition that should be interpreted in any group takes, as
arguments, the type of the group and the group structure as arguments.
Similarly, a theorem about the elements of an arbitrary group
begins with universal quantifiers over
the type of the group and the group structure.</p></li>
<li><p><em>Implicit arguments.</em> The arguments for the type and the structure
are generally left implicit, so that we do not have to write them
or see them in the Lean information window. Lean fills the
information in for us silently.</p></li>
<li><p><em>Type class inference.</em> Also known as <em>class inference</em>,
this is a simple but powerful mechanism
that enables us to register information for Lean to use later on.
When Lean is called on to fill in implicit arguments to a
definition, theorem, or piece of notation,
it can make use of information that has been registered.</p></li>
</ol>
<p>Whereas an annotation <code class="docutils literal notranslate"><span class="pre">(grp</span> <span class="pre">:</span> <span class="pre">Group</span> <span class="pre">G)</span></code> tells Lean that it should
expect to be given that argument explicitly and the annotation
<code class="docutils literal notranslate"><span class="pre">{grp</span> <span class="pre">:</span> <span class="pre">Group</span> <span class="pre">G}</span></code> tells Lean that it should try to figure it out
from contextual cues in the expression,
the annotation <code class="docutils literal notranslate"><span class="pre">[grp</span> <span class="pre">:</span> <span class="pre">Group</span> <span class="pre">G]</span></code> tells Lean that the corresponding
argument should be synthesized using type class inference.
Since the whole point to the use of such arguments is that
we generally do not need to refer to them explicitly,
Lean allows us to write <code class="docutils literal notranslate"><span class="pre">[Group</span> <span class="pre">G]</span></code> and leave the name anonymous.
You have probably already noticed that Lean chooses names like <code class="docutils literal notranslate"><span class="pre">_inst_1</span></code>
automatically.
When we use the anonymous square-bracket annotation with the <code class="docutils literal notranslate"><span class="pre">variables</span></code> command,
then as long as the variables are still in scope,
Lean automatically adds the argument <code class="docutils literal notranslate"><span class="pre">[Group</span> <span class="pre">G]</span></code> to any definition or
theorem that mentions <code class="docutils literal notranslate"><span class="pre">G</span></code>.</p>
<p>How do we register the information that Lean needs to use to carry
out the search?
Returning to our group example, we need only make two changes.
First, instead of using the <code class="docutils literal notranslate"><span class="pre">structure</span></code> command to define the group structure,
we use the keyword <code class="docutils literal notranslate"><span class="pre">class</span></code> to indicate that it is a candidate
for class inference.
Second, instead of defining particular instances with <code class="docutils literal notranslate"><span class="pre">def</span></code>,
we use the keyword <code class="docutils literal notranslate"><span class="pre">instance</span></code> to register the particular instance with
Lean. As with the names of class variables, we are allowed to leave the
name of an instance definition anonymous,
since in general we intend Lean to find it and put it to use
without troubling us with the details.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span><span class="w"> </span><span class="n">Group&#8322;</span><span class="w"> </span><span class="o">(</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">mul</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="n">one</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="n">inv</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="n">mul_assoc</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="o">(</span><span class="n">mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">(</span><span class="n">mul</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="o">)</span>
<span class="w">  </span><span class="n">mul_one</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">one</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">one_mul</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">one</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">inv_mul_cancel</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="o">(</span><span class="n">inv</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">one</span>

<span class="kd">instance</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Group&#8322;</span><span class="w"> </span><span class="o">(</span><span class="n">Equiv.Perm</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">mul</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.trans</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">f</span>
<span class="w">  </span><span class="n">one</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.refl</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="n">inv</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.symm</span>
<span class="w">  </span><span class="n">mul_assoc</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">Equiv.trans_assoc</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="o">)</span><span class="bp">.</span><span class="n">symm</span>
<span class="w">  </span><span class="n">one_mul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.trans_refl</span>
<span class="w">  </span><span class="n">mul_one</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.refl_trans</span>
<span class="w">  </span><span class="n">inv_mul_cancel</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Equiv.self_trans_symm</span>
</pre></div>
</div>
<p>The following illustrates their use.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">Group&#8322;.mul</span>

<span class="kd">def</span><span class="w"> </span><span class="n">mySquare</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group&#8322;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Group&#8322;.mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">x</span>

<span class="k">#check</span><span class="w"> </span><span class="n">mySquare</span>

<span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#946;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Equiv.Perm</span><span class="w"> </span><span class="n">&#946;</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Group&#8322;.mul</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">g.trans</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">mySquare</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f.trans</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>The <code class="docutils literal notranslate"><span class="pre">#check</span></code> command shows that <code class="docutils literal notranslate"><span class="pre">Group&#8322;.mul</span></code> has an implicit argument
<code class="docutils literal notranslate"><span class="pre">[Group&#8322;</span> <span class="pre">&#945;]</span></code> that we expect to be found by class inference,
where <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> is the type of the arguments to <code class="docutils literal notranslate"><span class="pre">Group&#8322;.mul</span></code>.
In other words, <code class="docutils literal notranslate"><span class="pre">{&#945;</span> <span class="pre">:</span> <span class="pre">Type*}</span></code> is the implicit argument for the type
of the group elements and <code class="docutils literal notranslate"><span class="pre">[Group&#8322;</span> <span class="pre">&#945;]</span></code> is the implicit argument for the
group structure on <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>.
Similarly, when we define a generic squaring function <code class="docutils literal notranslate"><span class="pre">my_square</span></code>
for <code class="docutils literal notranslate"><span class="pre">Group&#8322;</span></code>, we use an implicit argument <code class="docutils literal notranslate"><span class="pre">{&#945;</span> <span class="pre">:</span> <span class="pre">Type*}</span></code> for
the type of the elements and an implicit argument <code class="docutils literal notranslate"><span class="pre">[Group&#8322;</span> <span class="pre">&#945;]</span></code> for
the <code class="docutils literal notranslate"><span class="pre">Group&#8322;</span></code> structure.</p>
<p>In the first example,
when we write <code class="docutils literal notranslate"><span class="pre">Group&#8322;.mul</span> <span class="pre">f</span> <span class="pre">g</span></code>, the type of <code class="docutils literal notranslate"><span class="pre">f</span></code> and <code class="docutils literal notranslate"><span class="pre">g</span></code>
tells Lean that in the argument <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> to <code class="docutils literal notranslate"><span class="pre">Group&#8322;.mul</span></code>
has to be instantiated to <code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">&#946;</span></code>.
That means that Lean has to find an element of <code class="docutils literal notranslate"><span class="pre">Group&#8322;</span> <span class="pre">(Equiv.Perm</span> <span class="pre">&#946;)</span></code>.
The previous <code class="docutils literal notranslate"><span class="pre">instance</span></code> declaration tells Lean exactly how to do that.
Problem solved!</p>
<p>This simple mechanism for registering information so that Lean can find it
when it needs it is remarkably useful.
Here is one way it comes up.
In Lean&#8217;s foundation, a data type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> may be empty.
In a number of applications, however, it is useful to know that a
type has at least one element.
For example, the function <code class="docutils literal notranslate"><span class="pre">List.headI</span></code>, which returns the first
element of a list, can return the default value when the list is empty.
To make that work, the Lean library defines a class <code class="docutils literal notranslate"><span class="pre">Inhabited</span> <span class="pre">&#945;</span></code>,
which does nothing more than store a default value.
We can show that the <code class="docutils literal notranslate"><span class="pre">Point</span></code> type is an instance:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Inhabited</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="n">where</span><span class="w"> </span><span class="n">default</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">&#10216;</span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="o">&#10217;</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">default</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">([]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">List</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span><span class="bp">.</span><span class="n">headI</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">default</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>The class inference mechanism is also used for generic notation.
The expression <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">+</span> <span class="pre">y</span></code> is an abbreviation for <code class="docutils literal notranslate"><span class="pre">Add.add</span> <span class="pre">x</span> <span class="pre">y</span></code>
where&#8212;you guessed it&#8212;<code class="docutils literal notranslate"><span class="pre">Add</span> <span class="pre">&#945;</span></code> is a class that stores
a binary function on <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>.
Writing <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">+</span> <span class="pre">y</span></code> tells Lean to find a registered instance of <code class="docutils literal notranslate"><span class="pre">[Add.add</span> <span class="pre">&#945;]</span></code>
and use the corresponding function.
Below, we register the addition function for <code class="docutils literal notranslate"><span class="pre">Point</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Add</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="n">where</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Point.add</span>

<span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Point</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Point.add</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>In this way, we can assign the notation <code class="docutils literal notranslate"><span class="pre">+</span></code> to binary operations on other
types as well.</p>
<p>But we can do even better. We have seen that <code class="docutils literal notranslate"><span class="pre">*</span></code> can be used in any
group, <code class="docutils literal notranslate"><span class="pre">+</span></code> can be used in any additive group, and both can be used in
any ring.
When we define a new instance of a ring in Lean,
we don&#8217;t have to define <code class="docutils literal notranslate"><span class="pre">+</span></code> and <code class="docutils literal notranslate"><span class="pre">*</span></code> for that instance,
because Lean knows that these are defined for every ring.
We can use this method to specify notation for our <code class="docutils literal notranslate"><span class="pre">Group&#8322;</span></code> class:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group&#8322;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Mul</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="n">Group&#8322;.mul</span><span class="o">&#10217;</span>

<span class="kd">instance</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group&#8322;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">One</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="n">Group&#8322;.one</span><span class="o">&#10217;</span>

<span class="kd">instance</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group&#8322;</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Inv</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="n">Group&#8322;.inv</span><span class="o">&#10217;</span>

<span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Equiv.Perm</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g</span><span class="bp">&#8315;&#185;</span>

<span class="kd">def</span><span class="w"> </span><span class="n">foo</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">g.symm.trans</span><span class="w"> </span><span class="o">((</span><span class="n">Equiv.refl</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="bp">.</span><span class="n">trans</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>What makes this approach work is that Lean carries out a recursive search.
According to the instances we have declared, Lean can find an instance of
<code class="docutils literal notranslate"><span class="pre">Mul</span> <span class="pre">(Equiv.Perm</span> <span class="pre">&#945;)</span></code> by finding an
instance of <code class="docutils literal notranslate"><span class="pre">Group&#8322;</span> <span class="pre">(Equiv.Perm</span> <span class="pre">&#945;)</span></code>, and it can find an instance of
<code class="docutils literal notranslate"><span class="pre">Group&#8322;</span> <span class="pre">(Equiv.Perm</span> <span class="pre">&#945;)</span></code> because we have provided one.
Lean is capable of finding these two facts and chaining them together.</p>
<p>The example we have just given is dangerous, because Lean&#8217;s
library also has an instance of <code class="docutils literal notranslate"><span class="pre">Group</span> <span class="pre">(Equiv.Perm</span> <span class="pre">&#945;)</span></code>, and
multiplication is defined on any group.
So it is ambiguous as to which instance is found.
In fact, Lean favors more recent declarations unless you explicitly
specify a different priority.
Also, there is another way to tell Lean that one structure is an
instance of another, using the <code class="docutils literal notranslate"><span class="pre">extends</span></code> keyword.
This is how Mathlib specifies that, for example,
every commutative ring is a ring.
You can find more information in <a class="reference internal" href="C08_Hierarchies.html#hierarchies"><span class="std std-numref">Section 8</span></a> and in a
<a class="reference external" href="https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html#managing-type-class-inference">section on class inference</a> in <em>Theorem Proving in Lean</em>.</p>
<p>In general, it is a bad idea to specify a value of
<code class="docutils literal notranslate"><span class="pre">*</span></code> for an instance of an algebraic structure that already has
the notation defined.
Redefining the notion of <code class="docutils literal notranslate"><span class="pre">Group</span></code> in Lean is an artificial example.
In this case, however, both interpretations of the group notation unfold to
<code class="docutils literal notranslate"><span class="pre">Equiv.trans</span></code>, <code class="docutils literal notranslate"><span class="pre">Equiv.refl</span></code>, and <code class="docutils literal notranslate"><span class="pre">Equiv.symm</span></code>, in the same way.</p>
<p>As a similarly artificial exercise,
define a class <code class="docutils literal notranslate"><span class="pre">AddGroup&#8322;</span></code> in analogy to <code class="docutils literal notranslate"><span class="pre">Group&#8322;</span></code>.
Define the usual notation for addition, negation, and zero
on any <code class="docutils literal notranslate"><span class="pre">AddGroup&#8322;</span></code>
using the classes <code class="docutils literal notranslate"><span class="pre">Add</span></code>, <code class="docutils literal notranslate"><span class="pre">Neg</span></code>, and <code class="docutils literal notranslate"><span class="pre">Zero</span></code>.
Then show <code class="docutils literal notranslate"><span class="pre">Point</span></code> is an instance of <code class="docutils literal notranslate"><span class="pre">AddGroup&#8322;</span></code>.
Try it out and make sure that the additive group notation works for
elements of <code class="docutils literal notranslate"><span class="pre">Point</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span><span class="w"> </span><span class="n">AddGroup&#8322;</span><span class="w"> </span><span class="o">(</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">add</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#945;</span>
<span class="w">  </span><span class="c1">-- fill in the rest</span>
</pre></div>
</div>
<p>It is not a big problem that we have already declared instances
<code class="docutils literal notranslate"><span class="pre">Add</span></code>, <code class="docutils literal notranslate"><span class="pre">Neg</span></code>, and <code class="docutils literal notranslate"><span class="pre">Zero</span></code> for <code class="docutils literal notranslate"><span class="pre">Point</span></code> above.
Once again, the two ways of synthesizing the notation should come up
with the same answer.</p>
<p>Class inference is subtle, and you have to be careful when using it,
because it configures automation that invisibly governs the interpretation of
the expressions we type.
When used wisely, however, class inference is a powerful tool.
It is what makes algebraic reasoning possible in Lean.</p>
</section>
<section id="building-the-gaussian-integers">
<span id="section-building-the-gaussian-integers"></span><h2><span class="section-number">7.3. </span>Building the Gaussian Integers<a class="headerlink" href="#building-the-gaussian-integers" title="Link to this heading">&#61633;</a></h2>
<p>We will now illustrate the use of the algebraic hierarchy in Lean by
building an important mathematical object, the <em>Gaussian integers</em>,
and showing that it is a Euclidean domain. In other words, according to
the terminology we have been using, we will define the Gaussian integers
and show that they are an instance of the Euclidean domain structure.</p>
<p>In ordinary mathematical terms, the set of Gaussian integers <span class="math notranslate nohighlight">\(\Bbb{Z}[i]\)</span>
is the set of complex numbers <span class="math notranslate nohighlight">\(\{ a + b i \mid a, b \in \Bbb{Z}\}\)</span>.
But rather than define them as a subset of the complex numbers, our goal
here is to define them as a data type in their own right. We do this by
representing a Gaussian integer as a pair of integers, which we think of as the
<em>real</em> and <em>imaginary</em> parts.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[</span><span class="n">ext</span><span class="kd">]</span>
<span class="kd">structure</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">re</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span>
<span class="w">  </span><span class="n">im</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span>
</pre></div>
</div>
<p>We first show that the Gaussian integers have the structure of a ring,
with <code class="docutils literal notranslate"><span class="pre">0</span></code> defined to be <code class="docutils literal notranslate"><span class="pre">&#10216;0,</span> <span class="pre">0&#10217;</span></code>, <code class="docutils literal notranslate"><span class="pre">1</span></code> defined to be <code class="docutils literal notranslate"><span class="pre">&#10216;1,</span> <span class="pre">0&#10217;</span></code>, and
addition defined pointwise. To work out the definition of multiplication,
remember that we want the element <span class="math notranslate nohighlight">\(i\)</span>, represented by <code class="docutils literal notranslate"><span class="pre">&#10216;0,</span> <span class="pre">1&#10217;</span></code>, to
be a square root of <span class="math notranslate nohighlight">\(-1\)</span>. Thus we want</p>
<div class="math notranslate nohighlight">
\[\begin{split}(a + bi) (c + di) &amp; = ac + bci + adi + bd i^2 \\
  &amp; = (ac - bd) + (bc + ad)i.\end{split}\]</div>
<p>This explains the definition of <code class="docutils literal notranslate"><span class="pre">Mul</span></code> below.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Zero</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;&#10216;</span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="o">&#10217;&#10217;</span>

<span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">One</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;&#10216;</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="o">&#10217;&#10217;</span>

<span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Add</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">x.re</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y.re</span><span class="o">,</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y.im</span><span class="o">&#10217;&#10217;</span>

<span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Neg</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="o">&#10216;</span><span class="bp">-</span><span class="n">x.re</span><span class="o">,</span><span class="w"> </span><span class="bp">-</span><span class="n">x.im</span><span class="o">&#10217;&#10217;</span>

<span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Mul</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">x.re</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.re</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.im</span><span class="o">,</span><span class="w"> </span><span class="n">x.re</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.im</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.re</span><span class="o">&#10217;&#10217;</span>
</pre></div>
</div>
<p>As noted in <a class="reference internal" href="#section-structures"><span class="std std-numref">Section 7.1</span></a>, it is a good idea to put all the definitions
related to a data type in a namespace with the same name. Thus in the Lean
files associated with this chapter, these definitions are made in the
<code class="docutils literal notranslate"><span class="pre">GaussInt</span></code> namespace.</p>
<p>Notice that here we are defining the interpretations of the notation <code class="docutils literal notranslate"><span class="pre">0</span></code>,
<code class="docutils literal notranslate"><span class="pre">1</span></code>, <code class="docutils literal notranslate"><span class="pre">+</span></code>, <code class="docutils literal notranslate"><span class="pre">-</span></code>, and <code class="docutils literal notranslate"><span class="pre">*</span></code> directly, rather than naming them
<code class="docutils literal notranslate"><span class="pre">GaussInt.zero</span></code> and the like and assigning the notation to those.
It is often useful to have an explicit name for the definitions, for example,
to use with <code class="docutils literal notranslate"><span class="pre">simp</span></code> and <code class="docutils literal notranslate"><span class="pre">rw</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">zero_def</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="mi">0</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">&#10216;</span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">one_def</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">&#10216;</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">add_def</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">x.re</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y.re</span><span class="o">,</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y.im</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">neg_def</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">-</span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">&#10216;</span><span class="bp">-</span><span class="n">x.re</span><span class="o">,</span><span class="w"> </span><span class="bp">-</span><span class="n">x.im</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">mul_def</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">x.re</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.re</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.im</span><span class="o">,</span><span class="w"> </span><span class="n">x.re</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.im</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.re</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>It is also useful to name the rules that compute the real and imaginary
parts, and to declare them to the simplifier.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">zero_re</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="mi">0</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">zero_im</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="mi">0</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">one_re</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">one_im</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">add_re</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x.re</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y.re</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">add_im</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y.im</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">neg_re</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">-</span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">-</span><span class="n">x.re</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">neg_im</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">-</span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">-</span><span class="n">x.im</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">mul_re</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x.re</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.re</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.im</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">mul_im</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x.re</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.im</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.re</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>It is now surprisingly easy to show that the Gaussian integers are an instance
of a commutative ring. We are putting the structure concept to good use.
Each particular Gaussian integer is an instance of the <code class="docutils literal notranslate"><span class="pre">GaussInt</span></code> structure,
whereas the type <code class="docutils literal notranslate"><span class="pre">GaussInt</span></code> itself, together with the relevant operations, is an
instance of the <code class="docutils literal notranslate"><span class="pre">CommRing</span></code> structure. The <code class="docutils literal notranslate"><span class="pre">CommRing</span></code> structure, in turn,
extends the notational structures <code class="docutils literal notranslate"><span class="pre">Zero</span></code>, <code class="docutils literal notranslate"><span class="pre">One</span></code>, <code class="docutils literal notranslate"><span class="pre">Add</span></code>,
<code class="docutils literal notranslate"><span class="pre">Neg</span></code>, and <code class="docutils literal notranslate"><span class="pre">Mul</span></code>.</p>
<p>If you type <code class="docutils literal notranslate"><span class="pre">instance</span> <span class="pre">:</span> <span class="pre">CommRing</span> <span class="pre">GaussInt</span> <span class="pre">:=</span> <span class="pre">_</span></code>, click on the light bulb
that appears in VS Code, and then ask Lean to fill in a skeleton for the
structure definition, you will see a scary number of entries.
Jumping to the definition of the structure, however, shows that many of the
fields have default definitions that Lean will fill in for you automatically.
The essential ones appear in the definition below.
A special case are <code class="docutils literal notranslate"><span class="pre">nsmul</span></code> and <code class="docutils literal notranslate"><span class="pre">zsmul</span></code> which should be ignored for now
and will be explained in the next chapter.
In each case, the relevant
identity is proved by unfolding definitions, using the <code class="docutils literal notranslate"><span class="pre">ext</span></code> tactic
to reduce the identities to their real and imaginary components,
simplifying, and, if necessary, carrying out the relevant ring calculation in
the integers. Note that we could easily avoid repeating all this code, but
this is not the topic of the current discussion.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="n">instCommRing</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">CommRing</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">zero</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="mi">0</span>
<span class="w">  </span><span class="n">one</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="mi">1</span>
<span class="w">  </span><span class="n">add</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="bp">&#183;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="bp">&#183;</span><span class="o">)</span>
<span class="w">  </span><span class="n">neg</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="bp">-</span><span class="n">x</span>
<span class="w">  </span><span class="n">mul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="bp">&#183;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#183;</span><span class="o">)</span>
<span class="w">  </span><span class="n">nsmul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">nsmulRec</span>
<span class="w">  </span><span class="n">zsmul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">zsmulRec</span>
<span class="w">  </span><span class="n">add_assoc</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intros</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">ring</span>
<span class="w">  </span><span class="n">zero_add</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="n">add_zero</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="n">neg_add_cancel</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="n">add_comm</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intros</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">ring</span>
<span class="w">  </span><span class="n">mul_assoc</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intros</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">ring</span>
<span class="w">  </span><span class="n">one_mul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="n">mul_one</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="n">left_distrib</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intros</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">ring</span>
<span class="w">  </span><span class="n">right_distrib</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intros</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">ring</span>
<span class="w">  </span><span class="n">mul_comm</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intros</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">ring</span>
<span class="w">  </span><span class="n">zero_mul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intros</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="n">mul_zero</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intros</span>
<span class="w">    </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>
</pre></div>
</div>
<p>Lean&#8217;s library defines the class of <em>nontrivial</em> types to be types with at
least two distinct elements. In the context of a ring, this is equivalent
to saying that the zero is not equal to the one. Since some common theorems
depend on that fact, we may as well establish it now.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nontrivial</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">use</span><span class="w"> </span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Ne</span><span class="o">,</span><span class="w"> </span><span class="n">GaussInt.ext_iff</span><span class="o">]</span>
<span class="w">  </span><span class="n">simp</span>
</pre></div>
</div>
<p>We will now show that the Gaussian integers have an important additional
property. A <em>Euclidean domain</em> is a ring <span class="math notranslate nohighlight">\(R\)</span> equipped with a <em>norm</em>
function <span class="math notranslate nohighlight">\(N : R \to \mathbb{N}\)</span> with the following two properties:</p>
<ul class="simple">
<li><p>For every <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b \ne 0\)</span> in <span class="math notranslate nohighlight">\(R\)</span>, there are
<span class="math notranslate nohighlight">\(q\)</span> and <span class="math notranslate nohighlight">\(r\)</span> in <span class="math notranslate nohighlight">\(R\)</span> such that <span class="math notranslate nohighlight">\(a = bq + r\)</span> and
either <span class="math notranslate nohighlight">\(r = 0\)</span> or <span class="math notranslate nohighlight">\(N(r) &lt; N(b)\)</span>.</p></li>
<li><p>For every <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b \ne 0\)</span>, <span class="math notranslate nohighlight">\(N(a) \le N(ab)\)</span>.</p></li>
</ul>
<p>The ring of integers <span class="math notranslate nohighlight">\(\Bbb{Z}\)</span> with <span class="math notranslate nohighlight">\(N(a) = |a|\)</span> is an
archetypal example of a Euclidean domain.
In that case, we can take <span class="math notranslate nohighlight">\(q\)</span> to be the
result of integer division of <span class="math notranslate nohighlight">\(a\)</span> by <span class="math notranslate nohighlight">\(b\)</span> and <span class="math notranslate nohighlight">\(r\)</span>
to be the remainder. These functions are defined in Lean so that the
satisfy the following:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Eq.symm</span><span class="w"> </span><span class="o">(</span><span class="n">Int.ediv_add_emod</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Int.emod_nonneg</span><span class="w"> </span><span class="n">a</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="bp">|</span><span class="n">b</span><span class="bp">|</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Int.emod_lt_abs</span><span class="w"> </span><span class="n">a</span>
</pre></div>
</div>
<p>In an arbitrary ring, an element <span class="math notranslate nohighlight">\(a\)</span> is said to be a <em>unit</em> if it divides
<span class="math notranslate nohighlight">\(1\)</span>. A nonzero element <span class="math notranslate nohighlight">\(a\)</span> is said to be <em>irreducible</em> if it cannot
be written in the form <span class="math notranslate nohighlight">\(a = bc\)</span>
where neither <span class="math notranslate nohighlight">\(b\)</span> nor <span class="math notranslate nohighlight">\(c\)</span> is a unit. In the integers, every
irreducible element <span class="math notranslate nohighlight">\(a\)</span> is <em>prime</em>, which is to say, whenever <span class="math notranslate nohighlight">\(a\)</span>
divides a product <span class="math notranslate nohighlight">\(bc\)</span>, it divides either <span class="math notranslate nohighlight">\(b\)</span> or <span class="math notranslate nohighlight">\(c\)</span>. But
in other rings this property can fail. In the ring
<span class="math notranslate nohighlight">\(\Bbb{Z}[\sqrt{-5}]\)</span>, we have</p>
<div class="math notranslate nohighlight">
\[6 = 2 \cdot 3 = (1 + \sqrt{-5})(1 - \sqrt{-5}),\]</div>
<p>and the elements <span class="math notranslate nohighlight">\(2\)</span>, <span class="math notranslate nohighlight">\(3\)</span>, <span class="math notranslate nohighlight">\(1 + \sqrt{-5}\)</span>, and
<span class="math notranslate nohighlight">\(1 - \sqrt{-5}\)</span> are all irreducible, but they are not prime. For example,
<span class="math notranslate nohighlight">\(2\)</span> divides the product <span class="math notranslate nohighlight">\((1 + \sqrt{-5})(1 - \sqrt{-5})\)</span>,
but it does not divide either factor. In particular, we no longer have
unique factorization: the number <span class="math notranslate nohighlight">\(6\)</span> can be factored into irreducible
elements in more than one way.</p>
<p>In contrast, every Euclidean domain is a unique factorization domain, which
implies that every irreducible element is prime.
The axioms for a Euclidean domain imply that one can write any nonzero element
as a finite product of irreducible elements. They also imply that one can use
the Euclidean algorithm to find a greatest common divisor of any two
nonzero elements <code class="docutils literal notranslate"><span class="pre">a</span></code> and <code class="docutils literal notranslate"><span class="pre">b</span></code>, i.e. an element that is divisible by any
other common divisor. This, in turn, implies that factorization
into irreducible elements is unique up to multiplication by units.</p>
<p>We now show that the Gaussian integers are a Euclidean domain with
the norm defined by <span class="math notranslate nohighlight">\(N(a + bi) = (a + bi)(a - bi) = a^2 + b^2\)</span>.
The Gaussian integer <span class="math notranslate nohighlight">\(a - bi\)</span> is called the <em>conjugate</em> of <span class="math notranslate nohighlight">\(a + bi\)</span>.
It is not hard to check that for any complex numbers <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span>,
we have <span class="math notranslate nohighlight">\(N(xy) = N(x)N(y)\)</span>.</p>
<p>To see that this definition of the norm makes the Gaussian integers a Euclidean
domain, only the first property is challenging. Suppose
we want to write <span class="math notranslate nohighlight">\(a + bi = (c + di) q + r\)</span> for suitable <span class="math notranslate nohighlight">\(q\)</span>
and <span class="math notranslate nohighlight">\(r\)</span>. Treating <span class="math notranslate nohighlight">\(a + bi\)</span> and <span class="math notranslate nohighlight">\(c + di\)</span> as complex
numbers, carry out the division</p>
<div class="math notranslate nohighlight">
\[\frac{a + bi}{c + di} = \frac{(a + bi)(c - di)}{(c + di)(c-di)} =
  \frac{ac + bd}{c^2 + d^2} + \frac{bc -ad}{c^2+d^2} i.\]</div>
<p>The real and imaginary parts might not be integers, but we can round
them to the nearest integers <span class="math notranslate nohighlight">\(u\)</span> and <span class="math notranslate nohighlight">\(v\)</span>. We can then express the
right-hand side as <span class="math notranslate nohighlight">\((u + vi) + (u' + v'i)\)</span>, where
<span class="math notranslate nohighlight">\(u' + v'i\)</span> is the part left over. Note that we have
<span class="math notranslate nohighlight">\(|u'| \le 1/2\)</span> and <span class="math notranslate nohighlight">\(|v'| \le 1/2\)</span>, and hence</p>
<div class="math notranslate nohighlight">
\[N(u' + v' i) = (u')^2 + (v')^2 \le 1/4 + 1/4 \le 1/2.\]</div>
<p>Multiplying through by <span class="math notranslate nohighlight">\(c + di\)</span>, we have</p>
<div class="math notranslate nohighlight">
\[a + bi = (c + di) (u + vi) + (c + di) (u' + v'i).\]</div>
<p>Setting <span class="math notranslate nohighlight">\(q = u + vi\)</span> and <span class="math notranslate nohighlight">\(r = (c + di) (u' + v'i)\)</span>, we have
<span class="math notranslate nohighlight">\(a + bi = (c + di) q + r\)</span>, and we only need to
bound <span class="math notranslate nohighlight">\(N(r)\)</span>:</p>
<div class="math notranslate nohighlight">
\[N(r) = N(c + di)N(u' + v'i) \le N(c + di) \cdot 1/2 &lt; N(c + di).\]</div>
<p>The argument we just carried out requires viewing the Gaussian integers
as a subset of the complex numbers. One option for formalizing it in Lean
is therefore to embed the Gaussian integers in the complex numbers, embed
the integers in the Gaussian integers, define the rounding function from the
real numbers to the integers, and take great care to pass back and forth
between these number systems appropriately.
In fact, this is exactly the approach that is followed in Mathlib,
where the Gaussian integers themselves are constructed as a special case
of a ring of <em>quadratic integers</em>.
See the file <a class="reference external" href="https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean">GaussianInt.lean</a>.</p>
<p>Here we will instead carry out an argument that stays in the integers.
This illustrates a choice one commonly faces when formalizing mathematics.
Given an argument that requires concepts or machinery that is not already
in the library, one has two choices: either formalize the concepts and machinery
needed, or adapt the argument to make use of concepts and machinery you
already have.
The first choice is generally a good investment of time when the results
can be used in other contexts.
Pragmatically speaking, however, sometimes seeking a more elementary proof
is more efficient.</p>
<p>The usual quotient-remainder theorem for the integers says that for
every <span class="math notranslate nohighlight">\(a\)</span> and nonzero <span class="math notranslate nohighlight">\(b\)</span>, there are <span class="math notranslate nohighlight">\(q\)</span> and <span class="math notranslate nohighlight">\(r\)</span>
such that <span class="math notranslate nohighlight">\(a = b q + r\)</span> and <span class="math notranslate nohighlight">\(0 \le r &lt; b\)</span>.
Here we will make use of the following variation, which says that there
are <span class="math notranslate nohighlight">\(q'\)</span> and <span class="math notranslate nohighlight">\(r'\)</span> such that
<span class="math notranslate nohighlight">\(a = b q' + r'\)</span> and <span class="math notranslate nohighlight">\(|r'| \le b/2\)</span>.
You can check that if the value of <span class="math notranslate nohighlight">\(r\)</span> in the first statement
satisfies <span class="math notranslate nohighlight">\(r \le b/2\)</span>, we can take <span class="math notranslate nohighlight">\(q' = q\)</span> and <span class="math notranslate nohighlight">\(r' = r\)</span>,
and otherwise we can take <span class="math notranslate nohighlight">\(q' = q + 1\)</span> and <span class="math notranslate nohighlight">\(r' = r - b\)</span>.
We are grateful to Heather Macbeth for suggesting the following more
elegant approach, which avoids definition by cases.
We simply add <code class="docutils literal notranslate"><span class="pre">b</span> <span class="pre">/</span> <span class="pre">2</span></code> to <code class="docutils literal notranslate"><span class="pre">a</span></code> before dividing and then subtract it
from the remainder.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">div&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">b</span>

<span class="kd">def</span><span class="w"> </span><span class="n">mod&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">div&#39;_add_mod&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">div&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">mod&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">div&#39;</span><span class="o">,</span><span class="w"> </span><span class="n">mod&#39;</span><span class="o">]</span>
<span class="w">  </span><span class="n">linarith</span><span class="w"> </span><span class="o">[</span><span class="n">Int.ediv_add_emod</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="n">b</span><span class="o">]</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">abs_mod&#39;_le</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">|</span><span class="n">mod&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="bp">|</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mod&#39;</span><span class="o">,</span><span class="w"> </span><span class="n">abs_le</span><span class="o">]</span>
<span class="w">  </span><span class="n">constructor</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">linarith</span><span class="w"> </span><span class="o">[</span><span class="n">Int.emod_nonneg</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="n">h.ne&#39;</span><span class="o">]</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Int.emod_lt_of_pos</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Int.ediv_add_emod</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="mi">2</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Int.emod_lt_of_pos</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">zero_lt_two</span>
<span class="w">  </span><span class="n">linarith</span>
</pre></div>
</div>
<p>Note the use of our old friend, <code class="docutils literal notranslate"><span class="pre">linarith</span></code>. We will also need to express
<code class="docutils literal notranslate"><span class="pre">mod'</span></code> in terms of <code class="docutils literal notranslate"><span class="pre">div'</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">mod&#39;_eq</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">mod&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">div&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">linarith</span><span class="w"> </span><span class="o">[</span><span class="n">div&#39;_add_mod&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">]</span>
</pre></div>
</div>
<p>We will use the fact that <span class="math notranslate nohighlight">\(x^2 + y^2\)</span> is equal to zero if and only if
<span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> are both zero. As an exercise, we ask you to prove
that this holds in any ordered ring.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">sq_add_sq_eq_zero</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">LinearOrder</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">IsStrictOrderedRing</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span>
<span class="w">    </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We will put all the remaining definitions and theorems in this section
in the <code class="docutils literal notranslate"><span class="pre">GaussInt</span></code> namespace.
First, we define the <code class="docutils literal notranslate"><span class="pre">norm</span></code> function and ask you to establish
some of its properties.
The proofs are all short.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">x.re</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">norm_nonneg</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">norm_eq_zero</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">norm_pos</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">norm_mul</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Next we define the conjugate function:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="n">x.re</span><span class="o">,</span><span class="w"> </span><span class="bp">-</span><span class="n">x.im</span><span class="o">&#10217;</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">conj_re</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">conj</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x.re</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">conj_im</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">conj</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">-</span><span class="n">x.im</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">norm_conj</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="o">(</span><span class="n">conj</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">norm</span><span class="o">]</span>
</pre></div>
</div>
<p>Finally, we define division for the Gaussian integers
with the notation <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">/</span> <span class="pre">y</span></code>, that rounds the complex quotient to the nearest
Gaussian integer. We use our bespoke <code class="docutils literal notranslate"><span class="pre">Int.div'</span></code> for that purpose.
As we calculated above, if <code class="docutils literal notranslate"><span class="pre">x</span></code> is <span class="math notranslate nohighlight">\(a + bi\)</span> and <code class="docutils literal notranslate"><span class="pre">y</span></code> is <span class="math notranslate nohighlight">\(c + di\)</span>,
then the real and imaginary parts of <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">/</span> <span class="pre">y</span></code> are the nearest integers to</p>
<div class="math notranslate nohighlight">
\[\frac{ac + bd}{c^2 + d^2} \quad \text{and} \quad \frac{bc -ad}{c^2+d^2},\]</div>
<p>respectively. Here the numerators are the real and imaginary parts of
<span class="math notranslate nohighlight">\((a + bi) (c - di)\)</span>, and the denominators are both equal to the norm
of <span class="math notranslate nohighlight">\(c + di\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Div</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">Int.div&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="o">),</span><span class="w"> </span><span class="n">Int.div&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="o">)&#10217;&#10217;</span>
</pre></div>
</div>
<p>Having defined <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">/</span> <span class="pre">y</span></code>, We define <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">%</span> <span class="pre">y</span></code> to be the remainder,
<code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">-</span> <span class="pre">(x</span> <span class="pre">/</span> <span class="pre">y)</span> <span class="pre">*</span> <span class="pre">y</span></code>. As above, we record the definitions in the
theorems <code class="docutils literal notranslate"><span class="pre">div_def</span></code> and
<code class="docutils literal notranslate"><span class="pre">mod_def</span></code> so that we can use them with <code class="docutils literal notranslate"><span class="pre">simp</span></code> and <code class="docutils literal notranslate"><span class="pre">rw</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Mod</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">y</span><span class="o">)&#10217;</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">div_def</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">x</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">Int.div&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="o">),</span><span class="w"> </span><span class="n">Int.div&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="o">)&#10217;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">mod_def</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>These definitions immediately yield <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">=</span> <span class="pre">y</span> <span class="pre">*</span> <span class="pre">(x</span> <span class="pre">/</span> <span class="pre">y)</span> <span class="pre">+</span> <span class="pre">x</span> <span class="pre">%</span> <span class="pre">y</span></code> for every
<code class="docutils literal notranslate"><span class="pre">x</span></code> and <code class="docutils literal notranslate"><span class="pre">y</span></code>, so all we need to do is show that the norm of <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">%</span> <span class="pre">y</span></code> is
less than the norm of <code class="docutils literal notranslate"><span class="pre">y</span></code> when <code class="docutils literal notranslate"><span class="pre">y</span></code> is not zero.</p>
<p>We just defined the real and imaginary parts of <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">/</span> <span class="pre">y</span></code> to be
<code class="docutils literal notranslate"><span class="pre">div'</span> <span class="pre">(x</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y).re</span> <span class="pre">(norm</span> <span class="pre">y)</span></code> and <code class="docutils literal notranslate"><span class="pre">div'</span> <span class="pre">(x</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y).im</span> <span class="pre">(norm</span> <span class="pre">y)</span></code>,
respectively.
Calculating, we have</p>
<blockquote>
<div><p><code class="docutils literal notranslate"><span class="pre">(x</span> <span class="pre">%</span> <span class="pre">y)</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y</span> <span class="pre">=</span> <span class="pre">(x</span> <span class="pre">-</span> <span class="pre">x</span> <span class="pre">/</span> <span class="pre">y</span> <span class="pre">*</span> <span class="pre">y)</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y</span> <span class="pre">=</span> <span class="pre">x</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y</span> <span class="pre">-</span> <span class="pre">x</span> <span class="pre">/</span> <span class="pre">y</span> <span class="pre">*</span> <span class="pre">(y</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y)</span></code></p>
</div></blockquote>
<p>The real and imaginary parts of the right-hand side are exactly <code class="docutils literal notranslate"><span class="pre">mod'</span> <span class="pre">(x</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y).re</span> <span class="pre">(norm</span> <span class="pre">y)</span></code> and <code class="docutils literal notranslate"><span class="pre">mod'</span> <span class="pre">(x</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y).im</span> <span class="pre">(norm</span> <span class="pre">y)</span></code>.
By the properties of <code class="docutils literal notranslate"><span class="pre">div'</span></code> and <code class="docutils literal notranslate"><span class="pre">mod'</span></code>,
these are guaranteed to be less than or equal to <code class="docutils literal notranslate"><span class="pre">norm</span> <span class="pre">y</span> <span class="pre">/</span> <span class="pre">2</span></code>.
So we have</p>
<blockquote>
<div><p><code class="docutils literal notranslate"><span class="pre">norm</span> <span class="pre">((x</span> <span class="pre">%</span> <span class="pre">y)</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y)</span> <span class="pre">&#8804;</span> <span class="pre">(norm</span> <span class="pre">y</span> <span class="pre">/</span> <span class="pre">2)^2</span> <span class="pre">+</span> <span class="pre">(norm</span> <span class="pre">y</span> <span class="pre">/</span> <span class="pre">2)^2</span> <span class="pre">&#8804;</span> <span class="pre">(norm</span> <span class="pre">y</span> <span class="pre">/</span> <span class="pre">2)</span> <span class="pre">*</span> <span class="pre">norm</span> <span class="pre">y</span></code>.</p>
</div></blockquote>
<p>On the other hand, we have</p>
<blockquote>
<div><p><code class="docutils literal notranslate"><span class="pre">norm</span> <span class="pre">((x</span> <span class="pre">%</span> <span class="pre">y)</span> <span class="pre">*</span> <span class="pre">conj</span> <span class="pre">y)</span> <span class="pre">=</span> <span class="pre">norm</span> <span class="pre">(x</span> <span class="pre">%</span> <span class="pre">y)</span> <span class="pre">*</span> <span class="pre">norm</span> <span class="pre">(conj</span> <span class="pre">y)</span> <span class="pre">=</span> <span class="pre">norm</span> <span class="pre">(x</span> <span class="pre">%</span> <span class="pre">y)</span> <span class="pre">*</span> <span class="pre">norm</span> <span class="pre">y</span></code>.</p>
</div></blockquote>
<p>Dividing through by <code class="docutils literal notranslate"><span class="pre">norm</span> <span class="pre">y</span></code> we have <code class="docutils literal notranslate"><span class="pre">norm</span> <span class="pre">(x</span> <span class="pre">%</span> <span class="pre">y)</span> <span class="pre">&#8804;</span> <span class="pre">(norm</span> <span class="pre">y)</span> <span class="pre">/</span> <span class="pre">2</span> <span class="pre">&lt;</span> <span class="pre">norm</span> <span class="pre">y</span></code>,
as required.</p>
<p>This messy calculation is carried out in the next proof. We encourage you
to step through the details and see if you can find a nicer argument.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">norm_mod_lt</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hy</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">norm</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">y.norm</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">norm_y_pos</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">rwa</span><span class="w"> </span><span class="o">[</span><span class="n">norm_pos</span><span class="o">]</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">H1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">Int.mod&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">re</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="o">),</span><span class="w"> </span><span class="n">Int.mod&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">im</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="o">)&#10217;</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">ext</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">Int.mod&#39;_eq</span><span class="o">,</span><span class="w"> </span><span class="n">mod_def</span><span class="o">,</span><span class="w"> </span><span class="n">div_def</span><span class="o">,</span><span class="w"> </span><span class="n">norm</span><span class="o">]</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">ring</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">H2</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="k">calc</span>
<span class="w">      </span><span class="n">norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">conj</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="n">only</span><span class="w"> </span><span class="o">[</span><span class="n">norm_mul</span><span class="o">,</span><span class="w"> </span><span class="n">norm_conj</span><span class="o">]</span>
<span class="w">      </span><span class="n">_</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">|</span><span class="n">Int.mod&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">x.re</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.re</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.im</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">|</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span>
<span class="w">          </span><span class="bp">+</span><span class="w"> </span><span class="bp">|</span><span class="n">Int.mod&#39;</span><span class="w"> </span><span class="o">(</span><span class="bp">-</span><span class="o">(</span><span class="n">x.re</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.im</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x.im</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y.re</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">|</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">H1</span><span class="o">,</span><span class="w"> </span><span class="n">norm</span><span class="o">,</span><span class="w"> </span><span class="n">sq_abs</span><span class="o">]</span>
<span class="w">      </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="o">(</span><span class="n">y.norm</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="o">(</span><span class="n">y.norm</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">gcongr</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">Int.abs_mod&#39;_le</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">norm_y_pos</span>
<span class="w">      </span><span class="n">_</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">ring</span>
<span class="w">      </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">gcongr</span><span class="bp">;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">Int.ediv_mul_le</span><span class="bp">;</span><span class="w"> </span><span class="n">norm_num</span>
<span class="w">  </span><span class="k">calc</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">le_of_mul_le_mul_right</span><span class="w"> </span><span class="n">H2</span><span class="w"> </span><span class="n">norm_y_pos</span>
<span class="w">    </span><span class="n">_</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">norm</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">        </span><span class="n">apply</span><span class="w"> </span><span class="n">Int.ediv_lt_of_lt_mul</span>
<span class="w">        </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">norm_num</span>
<span class="w">        </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">linarith</span>
</pre></div>
</div>
<p>We are in the home stretch. Our <code class="docutils literal notranslate"><span class="pre">norm</span></code> function maps Gaussian integers to
nonnegative integers. We need a function that maps Gaussian integers to natural
numbers, and we obtain that by composing <code class="docutils literal notranslate"><span class="pre">norm</span></code> with the function
<code class="docutils literal notranslate"><span class="pre">Int.natAbs</span></code>, which maps integers to the natural numbers.
The first of the next two lemmas establishes that mapping the norm to the
natural numbers and back to the integers does not change the value.
The second one re-expresses the fact that the norm is decreasing.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">coe_natAbs_norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x.norm.natAbs</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x.norm</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Int.natAbs_of_nonneg</span><span class="w"> </span><span class="o">(</span><span class="n">norm_nonneg</span><span class="w"> </span><span class="n">_</span><span class="o">)</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">natAbs_norm_mod_lt</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hy</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">norm.natAbs</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">y.norm.natAbs</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">Int.ofNat_lt</span><span class="bp">.</span><span class="mi">1</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="n">only</span><span class="w"> </span><span class="o">[</span><span class="n">Int.natCast_natAbs</span><span class="o">,</span><span class="w"> </span><span class="n">abs_of_nonneg</span><span class="o">,</span><span class="w"> </span><span class="n">norm_nonneg</span><span class="o">]</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">norm_mod_lt</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">hy</span>
</pre></div>
</div>
<p>We also need to establish the second key property of the norm function
on a Euclidean domain.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">not_norm_mul_left_lt_norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hy</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#172;</span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="o">))</span><span class="bp">.</span><span class="n">natAbs</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="o">(</span><span class="n">norm</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">natAbs</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">not_lt_of_ge</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">norm_mul</span><span class="o">,</span><span class="w"> </span><span class="n">Int.natAbs_mul</span><span class="o">]</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">le_mul_of_one_le_right</span><span class="w"> </span><span class="o">(</span><span class="n">Nat.zero_le</span><span class="w"> </span><span class="n">_</span><span class="o">)</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">Int.ofNat_le</span><span class="bp">.</span><span class="mi">1</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">coe_natAbs_norm</span><span class="o">]</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">Int.add_one_le_of_lt</span><span class="w"> </span><span class="o">((</span><span class="n">norm_pos</span><span class="w"> </span><span class="n">_</span><span class="o">)</span><span class="bp">.</span><span class="n">mpr</span><span class="w"> </span><span class="n">hy</span><span class="o">)</span>
</pre></div>
</div>
<p>We can now put it together to show that the Gaussian integers are an
instance of a Euclidean domain. We use the quotient and remainder function we
have defined.
The Mathlib definition of a Euclidean domain is more general than the one
above in that it allows us to show that remainder decreases with respect
to any well-founded measure.
Comparing the values of a norm function that returns natural numbers is
just one instance of such a measure,
and in that case, the required properties are the theorems
<code class="docutils literal notranslate"><span class="pre">natAbs_norm_mod_lt</span></code> and <code class="docutils literal notranslate"><span class="pre">not_norm_mul_left_lt_norm</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">EuclideanDomain</span><span class="w"> </span><span class="n">GaussInt</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">{</span><span class="w"> </span><span class="n">GaussInt.instCommRing</span><span class="w"> </span><span class="k">with</span>
<span class="w">    </span><span class="n">quotient</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="bp">&#183;</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="bp">&#183;</span><span class="o">)</span>
<span class="w">    </span><span class="n">remainder</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="bp">&#183;</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="bp">&#183;</span><span class="o">)</span>
<span class="w">    </span><span class="n">quotient_mul_add_remainder_eq</span><span class="w"> </span><span class="o">:=</span>
<span class="w">      </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mod_def</span><span class="o">,</span><span class="w"> </span><span class="n">add_comm</span><span class="o">]</span><span class="w"> </span><span class="bp">;</span><span class="w"> </span><span class="n">ring</span>
<span class="w">    </span><span class="n">quotient_zero</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="kd">by</span>
<span class="w">      </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">div_def</span><span class="o">,</span><span class="w"> </span><span class="n">norm</span><span class="o">,</span><span class="w"> </span><span class="n">Int.div&#39;</span><span class="o">]</span>
<span class="w">      </span><span class="n">rfl</span>
<span class="w">    </span><span class="n">r</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">measure</span><span class="w"> </span><span class="o">(</span><span class="n">Int.natAbs</span><span class="w"> </span><span class="bp">&#8728;</span><span class="w"> </span><span class="n">norm</span><span class="o">))</span><span class="bp">.</span><span class="mi">1</span>
<span class="w">    </span><span class="n">r_wellFounded</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">measure</span><span class="w"> </span><span class="o">(</span><span class="n">Int.natAbs</span><span class="w"> </span><span class="bp">&#8728;</span><span class="w"> </span><span class="n">norm</span><span class="o">))</span><span class="bp">.</span><span class="mi">2</span>
<span class="w">    </span><span class="n">remainder_lt</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">natAbs_norm_mod_lt</span>
<span class="w">    </span><span class="n">mul_left_not_lt</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">not_norm_mul_left_lt_norm</span><span class="w"> </span><span class="o">}</span>
</pre></div>
</div>
<p>An immediate payoff is that we now know that, in the Gaussian integers,
the notions of being prime and being irreducible coincide.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Irreducible</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">Prime</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">irreducible_iff_prime</span>
</pre></div>
</div>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="C06_Discrete_Mathematics.html" class="btn btn-neutral float-left" title="6. Discrete Mathematics" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="C08_Hierarchies.html" class="btn btn-neutral float-right" title="8. Hierarchies" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <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>