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

<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<head>
  <meta charset="utf-8" />
  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>7. Hierarchies &mdash; Mathematics in Lean 0.1 documentation</title>
      <link rel="stylesheet" href="_static/pygments.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/custom.css" type="text/css" />
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
        <script src="_static/jquery.js"></script>
        <script src="_static/underscore.js"></script>
        <script src="_static/doctools.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. Groups and Rings" href="C08_Groups_and_Rings.html" />
    <link rel="prev" title="6. Structures" href="C06_Structures.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" />
    <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_Structures.html">6. Structures</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">7. Hierarchies</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#basics">7.1. Basics</a></li>
<li class="toctree-l2"><a class="reference internal" href="#morphisms">7.2. Morphisms</a></li>
<li class="toctree-l2"><a class="reference internal" href="#sub-objects">7.3. Sub-objects</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C08_Groups_and_Rings.html">8. Groups and Rings</a></li>
<li class="toctree-l1"><a class="reference internal" href="C09_Topology.html">9. Topology</a></li>
<li class="toctree-l1"><a class="reference internal" href="C10_Differential_Calculus.html">10. Differential Calculus</a></li>
<li class="toctree-l1"><a class="reference internal" href="C11_Integration_and_Measure_Theory.html">11. 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"></a> &raquo;</li>
      <li><span class="section-number">7. </span>Hierarchies</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/C07_Hierarchies.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">
             
  <div class="section" id="hierarchies">
<span id="id1"></span><h1><span class="section-number">7. </span>Hierarchies<a class="headerlink" href="#hierarchies" title="Permalink to this headline">&#61633;</a></h1>
<p>We have seen in <a class="reference internal" href="C06_Structures.html#structures"><span class="std std-numref">Chapter 6</span></a> how to define the class
of groups and build instances of this class, and then how to build an instance
of the commutative ring class. But of course there is a hierarchy here: a
commutative ring is in particular an additive group. In this chapter we
will study how to build such hierarchies. They appear in all branches
of mathematics but in this chapter the emphasis will be on algebraic examples.</p>
<p>It may seem premature to discuss how to build hierarchies before more discussions
about using existing hierarchies. But some understanding of the technology underlying
hierarchies is required to use them. So you should probably still read this chapter,
but without trying too hard to remember everything on your first read, then read
the following chapters and come back here for a second reading.</p>
<p>In this chapter, we will redefine (simpler versions of) many things that appear in Mathlib
so we will used indices to distinguish our version. For instance we will have <code class="docutils literal notranslate"><span class="pre">Ring&#8321;</span></code>
as our version of <code class="docutils literal notranslate"><span class="pre">Ring</span></code>. Since we will gradually explain more powerful ways of formalizing
structures, those indices will sometimes grow beyond one.</p>
<div class="section" id="basics">
<span id="section-hierarchies-basics"></span><h2><span class="section-number">7.1. </span>Basics<a class="headerlink" href="#basics" title="Permalink to this headline">&#61633;</a></h2>
<p>At the very bottom of all hierarchies in Lean, we find data-carrying
classes. The following class records that the given type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> is endowed with
a distinguished element called <code class="docutils literal notranslate"><span class="pre">one</span></code>. At this stage, it has no property at all.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">One&#8321;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="n">where</span>
  <span class="sd">/-- The element one -/</span>
  <span class="n">one</span> <span class="o">:</span> <span class="n">&#945;</span>
</pre></div>
</div>
<p>Since we&#8217;ll make a much heavier use of classes in this chapter, we need to understand some
more details about what the <code class="docutils literal notranslate"><span class="pre">class</span></code> command is doing.
First, the <code class="docutils literal notranslate"><span class="pre">class</span></code> command above defines a structure <code class="docutils literal notranslate"><span class="pre">One&#8321;</span></code> with parameter <code class="docutils literal notranslate"><span class="pre">&#945;</span> <span class="pre">:</span> <span class="pre">Type</span></code> and
a single field <code class="docutils literal notranslate"><span class="pre">one</span></code>. It also mark this structure as a class so that arguments of type
<code class="docutils literal notranslate"><span class="pre">One&#8321;</span> <span class="pre">&#945;</span></code> for some type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> will be inferrable using the instance resolution procedure,
as long as they are marked as instance-implicit, ie appear between square brackets.
Those two effects could also have been achieved using the <code class="docutils literal notranslate"><span class="pre">structure</span></code> command with <code class="docutils literal notranslate"><span class="pre">class</span></code>
attribute, ie writing <code class="docutils literal notranslate"><span class="pre">&#64;[class]</span> <span class="pre">structure</span></code> instance of <code class="docutils literal notranslate"><span class="pre">class</span></code>. But the class command also
ensures that <code class="docutils literal notranslate"><span class="pre">One&#8321;</span> <span class="pre">&#945;</span></code> appears as an instance-implicit argument in its own fields. Compare:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span> <span class="n">One&#8321;.one</span> <span class="c1">-- One&#8321;.one {&#945; : Type} [self : One&#8321; &#945;] : &#945;</span>

<span class="kd">@[class]</span> <span class="kd">structure</span> <span class="n">One&#8322;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="n">where</span>
  <span class="sd">/-- The element one -/</span>
  <span class="n">one</span> <span class="o">:</span> <span class="n">&#945;</span>

<span class="k">#check</span> <span class="n">One&#8322;.one</span>
</pre></div>
</div>
<p>In the second check, we can see that <code class="docutils literal notranslate"><span class="pre">self</span> <span class="pre">:</span> <span class="pre">One&#8322;</span> <span class="pre">&#945;</span></code> is an explicit argument.
Let us make sure the first version is indeed usable without any explicit argument.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">One&#8321;</span> <span class="n">&#945;</span><span class="o">]</span> <span class="o">:</span> <span class="n">&#945;</span> <span class="o">:=</span> <span class="n">One&#8321;.one</span>
</pre></div>
</div>
<p>Remark: in the above example, the argument <code class="docutils literal notranslate"><span class="pre">One&#8321;</span> <span class="pre">&#945;</span></code> is marked as instance-implicit,
which is a bit silly since this affects only <em>uses</em> of the declaration and declaration created by
the <code class="docutils literal notranslate"><span class="pre">example</span></code> command cannot be used. However it allows us to avoid giving a name to that
argument and, more importantly, it starts installing the good habit of marking <code class="docutils literal notranslate"><span class="pre">One&#8321;</span> <span class="pre">&#945;</span></code>
arguments as instance-implicit.</p>
<p>Another remark is that all this will work only when Lean knows what is <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>. In the above
example, leaving out the type ascription <code class="docutils literal notranslate"><span class="pre">:</span> <span class="pre">&#945;</span></code> would generate an error message like:
<code class="docutils literal notranslate"><span class="pre">typeclass</span> <span class="pre">instance</span> <span class="pre">problem</span> <span class="pre">is</span> <span class="pre">stuck,</span> <span class="pre">it</span> <span class="pre">is</span> <span class="pre">often</span> <span class="pre">due</span> <span class="pre">to</span> <span class="pre">metavariables</span> <span class="pre">One&#8321;</span> <span class="pre">(?m.263</span> <span class="pre">&#945;)</span></code>
where <code class="docutils literal notranslate"><span class="pre">?m.263</span> <span class="pre">&#945;</span></code> means &#8220;some type depending on <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>&#8221; (and 263 is simply an auto-generated
index that would be useful to distinguish between several unknown things). Another way
to avoid this issue would be to use a type annotation, as in:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">One&#8321;</span> <span class="n">&#945;</span><span class="o">]</span> <span class="o">:=</span> <span class="o">(</span><span class="n">One&#8321;.one</span> <span class="o">:</span> <span class="n">&#945;</span><span class="o">)</span>
</pre></div>
</div>
<p>You may have already encountered that issue when playing with limits of sequences
in <a class="reference internal" href="C03_Logic.html#sequences-and-convergence"><span class="std std-numref">Section 3.6</span></a> if you tried to state for instance that
<code class="docutils literal notranslate"><span class="pre">0</span> <span class="pre">&lt;</span> <span class="pre">1</span></code> without telling Lean whether you meant this inequality to be about natural numbers
or real numbers.</p>
<p>Our next task is to assign a notation to <code class="docutils literal notranslate"><span class="pre">One&#8321;.one</span></code>. Since we don&#8217;t want collisions
with the builtin notation for <code class="docutils literal notranslate"><span class="pre">1</span></code>, we will use <code class="docutils literal notranslate"><span class="pre">&#120793;</span></code>. This is achieved by the following
command where the first line tells Lean to use the documentation
of <code class="docutils literal notranslate"><span class="pre">One&#8321;.one</span></code> as documentation for the symbol <code class="docutils literal notranslate"><span class="pre">&#120793;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[inherit_doc]</span>
<span class="kd">notation</span> <span class="s2">&quot;&#120793;&quot;</span> <span class="bp">=&gt;</span> <span class="n">One&#8321;.one</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">}</span> <span class="o">[</span><span class="n">One&#8321;</span> <span class="n">&#945;</span><span class="o">]</span> <span class="o">:</span> <span class="n">&#945;</span> <span class="o">:=</span> <span class="mi">&#120793;</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">}</span> <span class="o">[</span><span class="n">One&#8321;</span> <span class="n">&#945;</span><span class="o">]</span> <span class="o">:</span> <span class="o">(</span><span class="mi">&#120793;</span> <span class="o">:</span> <span class="n">&#945;</span><span class="o">)</span> <span class="bp">=</span> <span class="mi">&#120793;</span> <span class="o">:=</span> <span class="n">rfl</span>
</pre></div>
</div>
<p>We now want a data-carrying class recording a binary operation. We don&#8217;t want to choose
between addition and multiplication for now so we&#8217;ll use diamond.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">Dia&#8321;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="n">where</span>
  <span class="n">dia</span> <span class="o">:</span> <span class="n">&#945;</span> <span class="bp">&#8594;</span> <span class="n">&#945;</span> <span class="bp">&#8594;</span> <span class="n">&#945;</span>

<span class="kd">infixl</span><span class="o">:</span><span class="mi">70</span> <span class="s2">&quot; &#8900; &quot;</span>   <span class="bp">=&gt;</span> <span class="n">Dia&#8321;.dia</span>
</pre></div>
</div>
<p>As in the <code class="docutils literal notranslate"><span class="pre">One&#8321;</span></code> example, the operation has no property at all at this stage. Let us
now define the class of semigroup structures where the operation is denoted by <code class="docutils literal notranslate"><span class="pre">&#8900;</span></code>.
For now, we define it by hand as a structure with two fields, a <code class="docutils literal notranslate"><span class="pre">Dia&#8321;</span></code> instance and some
<code class="docutils literal notranslate"><span class="pre">Prop</span></code>-valued field <code class="docutils literal notranslate"><span class="pre">dia_assoc</span></code> asserting associativity of <code class="docutils literal notranslate"><span class="pre">&#8900;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">Semigroup&#8321;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="n">where</span>
  <span class="n">toDia&#8321;</span> <span class="o">:</span> <span class="n">Dia&#8321;</span> <span class="n">&#945;</span>
  <span class="sd">/-- Diamond is associative -/</span>
  <span class="n">dia_assoc</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">&#945;</span><span class="o">,</span> <span class="n">a</span> <span class="bp">&#8900;</span> <span class="n">b</span> <span class="bp">&#8900;</span> <span class="n">c</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">&#8900;</span> <span class="o">(</span><span class="n">b</span> <span class="bp">&#8900;</span> <span class="n">c</span><span class="o">)</span>
</pre></div>
</div>
<p>Note that while stating <cite>dia_assoc</cite>, the previously defined field <cite>toDia&#8321;</cite> is in the local
context hence can be used when Lean searches for an instance of <cite>Dia&#8321; &#945;</cite> to make sense
of <cite>a &#8900; b</cite>. However this <cite>toDia&#8321;</cite> field does not become part of the type class instances database.
Hence doing <code class="docutils literal notranslate"><span class="pre">example</span> <span class="pre">{&#945;</span> <span class="pre">:</span> <span class="pre">Type}</span> <span class="pre">[Semigroup&#8321;</span> <span class="pre">&#945;]</span> <span class="pre">(a</span> <span class="pre">b</span> <span class="pre">:</span> <span class="pre">&#945;)</span> <span class="pre">:</span> <span class="pre">&#945;</span> <span class="pre">:=</span> <span class="pre">a</span> <span class="pre">&#8900;</span> <span class="pre">b</span></code> would fail with
error message <code class="docutils literal notranslate"><span class="pre">failed</span> <span class="pre">to</span> <span class="pre">synthesize</span> <span class="pre">instance</span> <span class="pre">Dia&#8321;</span> <span class="pre">&#945;</span></code>.</p>
<p>We can fix this by adding the <code class="docutils literal notranslate"><span class="pre">instance</span></code> attribute later.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">attribute</span> <span class="o">[</span><span class="kd">instance</span><span class="o">]</span> <span class="n">Semigroup&#8321;.toDia&#8321;</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">}</span> <span class="o">[</span><span class="n">Semigroup&#8321;</span> <span class="n">&#945;</span><span class="o">]</span> <span class="o">(</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#945;</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#945;</span> <span class="o">:=</span> <span class="n">a</span> <span class="bp">&#8900;</span> <span class="n">b</span>
</pre></div>
</div>
<p>Before building up, we need a more convenient way to extend structures than explicitly
writing fields like <cite>toDia&#8321;</cite> and adding the instance attribute by hand. The <code class="docutils literal notranslate"><span class="pre">class</span></code>
supports this using the <code class="docutils literal notranslate"><span class="pre">extends</span></code> syntax as in:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">Semigroup&#8322;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">Dia&#8321;</span> <span class="n">&#945;</span> <span class="n">where</span>
  <span class="sd">/-- Diamond is associative -/</span>
  <span class="n">dia_assoc</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">&#945;</span><span class="o">,</span> <span class="n">a</span> <span class="bp">&#8900;</span> <span class="n">b</span> <span class="bp">&#8900;</span> <span class="n">c</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">&#8900;</span> <span class="o">(</span><span class="n">b</span> <span class="bp">&#8900;</span> <span class="n">c</span><span class="o">)</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">}</span> <span class="o">[</span><span class="n">Semigroup&#8322;</span> <span class="n">&#945;</span><span class="o">]</span> <span class="o">(</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#945;</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#945;</span> <span class="o">:=</span> <span class="n">a</span> <span class="bp">&#8900;</span> <span class="n">b</span>
</pre></div>
</div>
<p>Note this syntax is also available in the <code class="docutils literal notranslate"><span class="pre">structure</span></code> command, although it that
case it fixes only the hurdle of writing fields such as <cite>toDia&#8321;</cite> since there
is no instance to define in that case.</p>
<p>Let us now try to combine a diamond operation and a distinguished one with axioms saying
this element is neutral on both sides.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">DiaOneClass&#8321;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">One&#8321;</span> <span class="n">&#945;</span><span class="o">,</span> <span class="n">Dia&#8321;</span> <span class="n">&#945;</span> <span class="n">where</span>
  <span class="sd">/-- One is a left neutral element for diamond. -/</span>
  <span class="n">one_dia</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">a</span> <span class="o">:</span> <span class="n">&#945;</span><span class="o">,</span> <span class="mi">&#120793;</span> <span class="bp">&#8900;</span> <span class="n">a</span> <span class="bp">=</span> <span class="n">a</span>
  <span class="sd">/-- One is a right neutral element for diamond -/</span>
  <span class="n">dia_one</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">a</span> <span class="o">:</span> <span class="n">&#945;</span><span class="o">,</span> <span class="n">a</span> <span class="bp">&#8900;</span> <span class="mi">&#120793;</span> <span class="bp">=</span> <span class="n">a</span>
</pre></div>
</div>
<p>In the next example, we tell Lean that <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> has a <code class="docutils literal notranslate"><span class="pre">DiaOneClass&#8321;</span></code> structure and state a
property that uses both a <cite>Dia&#8321;</cite> instance and a <cite>One&#8321;</cite> instance. In order to see how Lean finds
those instances we set a tracing option whose result can be seen in the Infoview. This result
is rather terse by default but it can be expanded by clicking on lines ending with black arrows.
It includes failed attempts where Lean tried to find instances before having enough type
information to succeed. The successful attempts do involve the instances generated by the
<code class="docutils literal notranslate"><span class="pre">extends</span></code> syntax.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">set_option</span> <span class="n">trace.Meta.synthInstance</span> <span class="n">true</span> <span class="k">in</span>
<span class="kd">example</span> <span class="o">{</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">}</span> <span class="o">[</span><span class="n">DiaOneClass&#8321;</span> <span class="n">&#945;</span><span class="o">]</span> <span class="o">(</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#945;</span><span class="o">)</span> <span class="o">:</span> <span class="kt">Prop</span> <span class="o">:=</span> <span class="n">a</span> <span class="bp">&#8900;</span> <span class="n">b</span> <span class="bp">=</span> <span class="mi">&#120793;</span>
</pre></div>
</div>
<p>Note that we don&#8217;t need to include extra fields where combining existing classes. Hence we can
define monoids as:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">Monoid&#8321;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">Semigroup&#8321;</span> <span class="n">&#945;</span><span class="o">,</span> <span class="n">DiaOneClass&#8321;</span> <span class="n">&#945;</span>
</pre></div>
</div>
<p>While the above definition seems straightforward, it hides an important subtlety. Both
<code class="docutils literal notranslate"><span class="pre">Semigroup&#8321;</span> <span class="pre">&#945;</span></code> and <code class="docutils literal notranslate"><span class="pre">DiaOneClass&#8321;</span> <span class="pre">&#945;</span></code> extend <code class="docutils literal notranslate"><span class="pre">Dia&#8321;</span> <span class="pre">&#945;</span></code>, so one could fear that having
a <code class="docutils literal notranslate"><span class="pre">Monoid&#8321;</span> <span class="pre">&#945;</span></code> instance gives two unrelated diamond operations on <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>, one coming from
a field <code class="docutils literal notranslate"><span class="pre">Monoid&#8321;.toSemigroup&#8321;</span></code> and one coming from a field <code class="docutils literal notranslate"><span class="pre">Monoid&#8321;.toDiaOneClass&#8321;</span></code>.</p>
<p>Indeed if we try to build a monoid class by hand using:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">Monoid&#8322;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="n">where</span>
  <span class="n">toSemigroup&#8321;</span> <span class="o">:</span> <span class="n">Semigroup&#8321;</span> <span class="n">&#945;</span>
  <span class="n">toDiaOneClass&#8321;</span> <span class="o">:</span> <span class="n">DiaOneClass&#8321;</span> <span class="n">&#945;</span>
</pre></div>
</div>
<p>then we get two completely unrelated diamond operations
<code class="docutils literal notranslate"><span class="pre">Monoid&#8322;.toSemigroup&#8321;.toDia&#8321;.dia</span></code> and <code class="docutils literal notranslate"><span class="pre">Monoid&#8322;.toDiaOneClass&#8321;.toDia&#8321;.dia</span></code>.</p>
<p>The version generated using the <code class="docutils literal notranslate"><span class="pre">extends</span></code> syntax does not have this defect.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">}</span> <span class="o">[</span><span class="n">Monoid&#8321;</span> <span class="n">&#945;</span><span class="o">]</span> <span class="o">:</span>
  <span class="o">(</span><span class="n">Monoid&#8321;.toSemigroup&#8321;.toDia&#8321;.dia</span> <span class="o">:</span> <span class="n">&#945;</span> <span class="bp">&#8594;</span> <span class="n">&#945;</span> <span class="bp">&#8594;</span> <span class="n">&#945;</span><span class="o">)</span> <span class="bp">=</span> <span class="n">Monoid&#8321;.toDiaOneClass&#8321;.toDia&#8321;.dia</span> <span class="o">:=</span> <span class="n">rfl</span>
</pre></div>
</div>
<p>So the <code class="docutils literal notranslate"><span class="pre">class</span></code> command did some magic for us (and the <code class="docutils literal notranslate"><span class="pre">structure</span></code> command would have done it
too). An easy way to see what are the fields of our classes is to check their constructor. Compare:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="c">/-</span><span class="cm"> Monoid&#8322;.mk {&#945; : Type} (toSemigroup&#8321; : Semigroup&#8321; &#945;) (toDiaOneClass&#8321; : DiaOneClass&#8321; &#945;) : Monoid&#8322; &#945; -/</span>
<span class="k">#check</span> <span class="n">Monoid&#8322;.mk</span>

<span class="c">/-</span><span class="cm"> Monoid&#8321;.mk {&#945; : Type} [toSemigroup&#8321; : Semigroup&#8321; &#945;] [toOne&#8321; : One&#8321; &#945;] (one_dia : &#8704; (a : &#945;), &#120793; &#8900; a = a) (dia_one : &#8704; (a : &#945;), a &#8900; &#120793; = a) : Monoid&#8321; &#945; -/</span>
<span class="k">#check</span> <span class="n">Monoid&#8321;.mk</span>
</pre></div>
</div>
<p>So we see that <code class="docutils literal notranslate"><span class="pre">Monoid&#8321;</span></code> takes <code class="docutils literal notranslate"><span class="pre">Semigroup&#8321;</span> <span class="pre">&#945;</span></code> argument as expected but then it won&#8217;t
take a would-be overlapping <code class="docutils literal notranslate"><span class="pre">DiaOneClass&#8321;</span> <span class="pre">&#945;</span></code> argument but instead tears it apart and includes
only the non-overlapping parts. And it also auto-generated an instance <code class="docutils literal notranslate"><span class="pre">Monoid&#8321;.toDiaOneClass&#8321;</span></code>
which is <em>not</em> a field but has the expected signature which, from the end-user point of view,
restores the symmetry between the two extended classes <code class="docutils literal notranslate"><span class="pre">Semigroup&#8321;</span></code> and <code class="docutils literal notranslate"><span class="pre">DiaOneClass&#8321;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span> <span class="n">Monoid&#8321;.toSemigroup&#8321;</span>
<span class="k">#check</span> <span class="n">Monoid&#8321;.toDiaOneClass&#8321;</span>
</pre></div>
</div>
<p>We are now very close to defining groups. We could add to the monoid structure a field asserting
the existence of an inverse for every element. But then we would need to work to access these
inverses. In practice it is more convenient to add it as data. To optimize reusability,
we define a new data-carrying class, and then give it some notation.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">Inv&#8321;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="n">where</span>
  <span class="sd">/-- The inversion function -/</span>
  <span class="n">inv</span> <span class="o">:</span> <span class="n">&#945;</span> <span class="bp">&#8594;</span> <span class="n">&#945;</span>

<span class="kd">@[inherit_doc]</span>
<span class="kd">postfix</span><span class="o">:</span><span class="n">max</span> <span class="s2">&quot;&#8315;&#185;&quot;</span> <span class="bp">=&gt;</span> <span class="n">Inv&#8321;.inv</span>

<span class="kd">class</span> <span class="n">Group&#8321;</span> <span class="o">(</span><span class="n">G</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">Monoid&#8321;</span> <span class="n">G</span><span class="o">,</span> <span class="n">Inv&#8321;</span> <span class="n">G</span> <span class="n">where</span>
  <span class="n">inv_dia</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">a</span> <span class="o">:</span> <span class="n">G</span><span class="o">,</span> <span class="n">a</span><span class="bp">&#8315;&#185;</span> <span class="bp">&#8900;</span> <span class="n">a</span> <span class="bp">=</span> <span class="mi">&#120793;</span>
</pre></div>
</div>
<p>The above definition may seem too weak, we only ask that <code class="docutils literal notranslate"><span class="pre">a&#8315;&#185;</span></code> is a left-inverse of <code class="docutils literal notranslate"><span class="pre">a</span></code>.
But the other side is automatic. In order to prove that, we need a preliminary lemma.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">lemma</span> <span class="n">left_inv_eq_right_inv&#8321;</span> <span class="o">{</span><span class="n">M</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">}</span> <span class="o">[</span><span class="n">Monoid&#8321;</span> <span class="n">M</span><span class="o">]</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">M</span><span class="o">}</span> <span class="o">(</span><span class="n">hba</span> <span class="o">:</span> <span class="n">b</span> <span class="bp">&#8900;</span> <span class="n">a</span> <span class="bp">=</span> <span class="mi">&#120793;</span><span class="o">)</span> <span class="o">(</span><span class="n">hac</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8900;</span> <span class="n">c</span> <span class="bp">=</span> <span class="mi">&#120793;</span><span class="o">)</span> <span class="o">:</span> <span class="n">b</span> <span class="bp">=</span> <span class="n">c</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">rw</span> <span class="o">[</span><span class="bp">&#8592;</span> <span class="n">DiaOneClass&#8321;.one_dia</span> <span class="n">c</span><span class="o">,</span> <span class="bp">&#8592;</span> <span class="n">hba</span><span class="o">,</span> <span class="n">Semigroup&#8321;.dia_assoc</span><span class="o">,</span> <span class="n">hac</span><span class="o">,</span> <span class="n">DiaOneClass&#8321;.dia_one</span> <span class="n">b</span><span class="o">]</span>
</pre></div>
</div>
<p>In this lemma, it is pretty annoying to give full names, especially since it requires knowing
which part of the hierarchy provides those facts. One way to fix this is to use the <code class="docutils literal notranslate"><span class="pre">export</span></code>
command to copy those facts as lemmas in the root name space.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">export</span> <span class="n">DiaOneClass&#8321;</span> <span class="o">(</span><span class="n">one_dia</span> <span class="n">dia_one</span><span class="o">)</span>
<span class="kn">export</span> <span class="n">Semigroup&#8321;</span> <span class="o">(</span><span class="n">dia_assoc</span><span class="o">)</span>
<span class="kn">export</span> <span class="n">Group&#8321;</span> <span class="o">(</span><span class="n">inv_dia</span><span class="o">)</span>
</pre></div>
</div>
<p>We can then rewrite the above proof as:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">M</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">}</span> <span class="o">[</span><span class="n">Monoid&#8321;</span> <span class="n">M</span><span class="o">]</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">M</span><span class="o">}</span> <span class="o">(</span><span class="n">hba</span> <span class="o">:</span> <span class="n">b</span> <span class="bp">&#8900;</span> <span class="n">a</span> <span class="bp">=</span> <span class="mi">&#120793;</span><span class="o">)</span> <span class="o">(</span><span class="n">hac</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8900;</span> <span class="n">c</span> <span class="bp">=</span> <span class="mi">&#120793;</span><span class="o">)</span> <span class="o">:</span> <span class="n">b</span> <span class="bp">=</span> <span class="n">c</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">rw</span> <span class="o">[</span><span class="bp">&#8592;</span> <span class="n">one_dia</span> <span class="n">c</span><span class="o">,</span> <span class="bp">&#8592;</span> <span class="n">hba</span><span class="o">,</span> <span class="n">dia_assoc</span><span class="o">,</span> <span class="n">hac</span><span class="o">,</span> <span class="n">dia_one</span> <span class="n">b</span><span class="o">]</span>
</pre></div>
</div>
<p>It is now your turn to prove things about our algebraic structures.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">lemma</span> <span class="n">inv_eq_of_dia</span> <span class="o">[</span><span class="n">Group&#8321;</span> <span class="n">G</span><span class="o">]</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">G</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8900;</span> <span class="n">b</span> <span class="bp">=</span> <span class="mi">&#120793;</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span><span class="bp">&#8315;&#185;</span> <span class="bp">=</span> <span class="n">b</span> <span class="o">:=</span>
  <span class="gr">sorry</span>

<span class="kd">lemma</span> <span class="n">dia_inv</span> <span class="o">[</span><span class="n">Group&#8321;</span> <span class="n">G</span><span class="o">]</span> <span class="o">(</span><span class="n">a</span> <span class="o">:</span> <span class="n">G</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8900;</span> <span class="n">a</span><span class="bp">&#8315;&#185;</span> <span class="bp">=</span> <span class="mi">&#120793;</span> <span class="o">:=</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<p>At this stage we would like to move on to define rings, but there is a serious issue.
A ring structure on a type contains both an additive group structure and a multiplicative
monoid structure, and some properties about their interaction. But so far we hard-coded
a notation <code class="docutils literal notranslate"><span class="pre">&#8900;</span></code> for all our operations. More fundamentally, the type class system
assumes every type has only one instance of each type class. There are various
ways to solve this issue. Surprisingly Mathlib uses the naive idea to duplicate
everything for additive and multiplicative theories with the help of some code-generating
attribute. Structures and classes are defined in both additive and multiplicative notation
with an attribute <code class="docutils literal notranslate"><span class="pre">to_additive</span></code> linking them. In case of multiple inheritance like for
semi-groups, the auto-generated &#8220;symmetry-restoring&#8221; instances need also to be marked.
This is a bit technical; you don&#8217;t need to understand details. The important point is that
lemmas are then only stated in multiplicative notation and marked with the attribute <code class="docutils literal notranslate"><span class="pre">to_additive</span></code>
to generate the additive version as <code class="docutils literal notranslate"><span class="pre">left_inv_eq_right_inv'</span></code> with its auto-generated additive
version <code class="docutils literal notranslate"><span class="pre">left_neg_eq_right_neg'</span></code>. In order to check the name of this additive version we
used the <code class="docutils literal notranslate"><span class="pre">whatsnew</span> <span class="pre">in</span></code> command on top of <code class="docutils literal notranslate"><span class="pre">left_inv_eq_right_inv'</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">AddSemigroup&#8323;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">Add</span> <span class="n">&#945;</span> <span class="n">where</span>
<span class="sd">/-- Addition is associative -/</span>
  <span class="n">add_assoc&#8323;</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">&#945;</span><span class="o">,</span> <span class="n">a</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">+</span> <span class="n">c</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">+</span> <span class="o">(</span><span class="n">b</span> <span class="bp">+</span> <span class="n">c</span><span class="o">)</span>

<span class="kd">@[to_additive AddSemigroup&#8323;]</span>
<span class="kd">class</span> <span class="n">Semigroup&#8323;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">Mul</span> <span class="n">&#945;</span> <span class="n">where</span>
<span class="sd">/-- Multiplication is associative -/</span>
  <span class="n">mul_assoc&#8323;</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">&#945;</span><span class="o">,</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">*</span> <span class="n">c</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">*</span> <span class="o">(</span><span class="n">b</span> <span class="bp">*</span> <span class="n">c</span><span class="o">)</span>

<span class="kd">class</span> <span class="n">AddMonoid&#8323;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">AddSemigroup&#8323;</span> <span class="n">&#945;</span><span class="o">,</span> <span class="n">AddZeroClass</span> <span class="n">&#945;</span>

<span class="kd">@[to_additive AddMonoid&#8323;]</span>
<span class="kd">class</span> <span class="n">Monoid&#8323;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">Semigroup&#8323;</span> <span class="n">&#945;</span><span class="o">,</span> <span class="n">MulOneClass</span> <span class="n">&#945;</span>

<span class="kn">attribute</span> <span class="o">[</span><span class="n">to_additive</span> <span class="n">existing</span><span class="o">]</span> <span class="n">Monoid&#8323;.toMulOneClass</span>

<span class="kn">export</span> <span class="n">Semigroup&#8323;</span> <span class="o">(</span><span class="n">mul_assoc&#8323;</span><span class="o">)</span>
<span class="kn">export</span> <span class="n">AddSemigroup&#8323;</span> <span class="o">(</span><span class="n">add_assoc&#8323;</span><span class="o">)</span>

<span class="n">whatsnew</span> <span class="k">in</span>
<span class="kd">@[to_additive]</span>
<span class="kd">lemma</span> <span class="n">left_inv_eq_right_inv&#39;</span> <span class="o">{</span><span class="n">M</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">}</span> <span class="o">[</span><span class="n">Monoid&#8323;</span> <span class="n">M</span><span class="o">]</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">M</span><span class="o">}</span> <span class="o">(</span><span class="n">hba</span> <span class="o">:</span> <span class="n">b</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">=</span> <span class="mi">1</span><span class="o">)</span> <span class="o">(</span><span class="n">hac</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">c</span> <span class="bp">=</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:</span> <span class="n">b</span> <span class="bp">=</span> <span class="n">c</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">rw</span> <span class="o">[</span><span class="bp">&#8592;</span> <span class="n">one_mul</span> <span class="n">c</span><span class="o">,</span> <span class="bp">&#8592;</span> <span class="n">hba</span><span class="o">,</span> <span class="n">mul_assoc&#8323;</span><span class="o">,</span> <span class="n">hac</span><span class="o">,</span> <span class="n">mul_one</span> <span class="n">b</span><span class="o">]</span>

<span class="k">#check</span> <span class="n">left_neg_eq_right_neg&#39;</span>
</pre></div>
</div>
<p>Equipped with this technology, we can easily define also commutative semigroups, monoids and
groups, and then define rings.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">AddCommSemigroup&#8323;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">AddSemigroup&#8323;</span> <span class="n">&#945;</span> <span class="n">where</span>
  <span class="n">add_comm</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#945;</span><span class="o">,</span> <span class="n">a</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">=</span> <span class="n">b</span> <span class="bp">+</span> <span class="n">a</span>

<span class="kd">@[to_additive AddCommSemigroup&#8323;]</span>
<span class="kd">class</span> <span class="n">CommSemigroup&#8323;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">Semigroup&#8323;</span> <span class="n">&#945;</span> <span class="n">where</span>
  <span class="n">mul_comm</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#945;</span><span class="o">,</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">=</span> <span class="n">b</span> <span class="bp">*</span> <span class="n">a</span>

<span class="kd">class</span> <span class="n">AddCommMonoid&#8323;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">AddMonoid&#8323;</span> <span class="n">&#945;</span><span class="o">,</span> <span class="n">AddCommSemigroup&#8323;</span> <span class="n">&#945;</span>

<span class="kd">@[to_additive AddCommMonoid&#8323;]</span>
<span class="kd">class</span> <span class="n">CommMonoid&#8323;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">Monoid&#8323;</span> <span class="n">&#945;</span><span class="o">,</span> <span class="n">CommSemigroup&#8323;</span> <span class="n">&#945;</span>

<span class="kd">class</span> <span class="n">AddGroup&#8323;</span> <span class="o">(</span><span class="n">G</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">AddMonoid&#8323;</span> <span class="n">G</span><span class="o">,</span> <span class="n">Neg</span> <span class="n">G</span> <span class="n">where</span>
  <span class="n">neg_add</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">a</span> <span class="o">:</span> <span class="n">G</span><span class="o">,</span> <span class="bp">-</span><span class="n">a</span> <span class="bp">+</span> <span class="n">a</span> <span class="bp">=</span> <span class="mi">0</span>

<span class="kd">@[to_additive AddGroup&#8323;]</span>
<span class="kd">class</span> <span class="n">Group&#8323;</span> <span class="o">(</span><span class="n">G</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">Monoid&#8323;</span> <span class="n">G</span><span class="o">,</span> <span class="n">Inv</span> <span class="n">G</span> <span class="n">where</span>
  <span class="n">inv_mul</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">a</span> <span class="o">:</span> <span class="n">G</span><span class="o">,</span> <span class="n">a</span><span class="bp">&#8315;&#185;</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">=</span> <span class="mi">1</span>
</pre></div>
</div>
<p>We should remember to tag lemmas with <code class="docutils literal notranslate"><span class="pre">simp</span></code> when appropriate.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">attribute</span> <span class="o">[</span><span class="n">simp</span><span class="o">]</span> <span class="n">Group&#8323;.inv_mul</span> <span class="n">AddGroup&#8323;.neg_add</span>
</pre></div>
</div>
<p>Then we need to repeat ourselves a bit since we switch to standard notations, but at least
<code class="docutils literal notranslate"><span class="pre">to_additive</span></code> does the work of translating from the multiplicative notation to the additive one.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[to_additive]</span>
<span class="kd">lemma</span> <span class="n">inv_eq_of_mul</span> <span class="o">[</span><span class="n">Group&#8323;</span> <span class="n">G</span><span class="o">]</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">G</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">=</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span><span class="bp">&#8315;&#185;</span> <span class="bp">=</span> <span class="n">b</span> <span class="o">:=</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<p>Note that <code class="docutils literal notranslate"><span class="pre">to_additive</span></code> can be asked to tag a lemma with <code class="docutils literal notranslate"><span class="pre">simp</span></code> and propagate that attribute
to the additive version as follows.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[to_additive (attr := simp)]</span>
<span class="kd">lemma</span> <span class="n">Group&#8323;.mul_inv</span> <span class="o">{</span><span class="n">G</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">}</span> <span class="o">[</span><span class="n">Group&#8323;</span> <span class="n">G</span><span class="o">]</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">G</span><span class="o">}</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">a</span><span class="bp">&#8315;&#185;</span> <span class="bp">=</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">@[to_additive]</span>
<span class="kd">lemma</span> <span class="n">mul_left_cancel&#8323;</span> <span class="o">{</span><span class="n">G</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">}</span> <span class="o">[</span><span class="n">Group&#8323;</span> <span class="n">G</span><span class="o">]</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">G</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">c</span><span class="o">)</span> <span class="o">:</span> <span class="n">b</span> <span class="bp">=</span> <span class="n">c</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">@[to_additive]</span>
<span class="kd">lemma</span> <span class="n">mul_right_cancel&#8323;</span> <span class="o">{</span><span class="n">G</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">}</span> <span class="o">[</span><span class="n">Group&#8323;</span> <span class="n">G</span><span class="o">]</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">G</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">b</span><span class="bp">*</span><span class="n">a</span> <span class="bp">=</span> <span class="n">c</span><span class="bp">*</span><span class="n">a</span><span class="o">)</span> <span class="o">:</span> <span class="n">b</span> <span class="bp">=</span> <span class="n">c</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">class</span> <span class="n">AddCommGroup&#8323;</span> <span class="o">(</span><span class="n">G</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">AddGroup&#8323;</span> <span class="n">G</span><span class="o">,</span> <span class="n">AddCommMonoid&#8323;</span> <span class="n">G</span>

<span class="kd">@[to_additive AddCommGroup&#8323;]</span>
<span class="kd">class</span> <span class="n">CommGroup&#8323;</span> <span class="o">(</span><span class="n">G</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">Group&#8323;</span> <span class="n">G</span><span class="o">,</span> <span class="n">CommMonoid&#8323;</span> <span class="n">G</span>
</pre></div>
</div>
<p>We are now ready for rings. For demonstration purposes we won&#8217;t assume that addition is
commutative, and then immediately provide an instance of <code class="docutils literal notranslate"><span class="pre">AddCommGroup&#8323;</span></code>. Mathlib does not
play this game, first because in practice this does not make any ring instance easier and
also because Mathlib&#8217;s algebraic hierarchy goes through semirings which are like rings but without
opposites so that the proof below does not work for them. What we gain here, besides a nice exercise
if you have never seen it, is an example of building an instance using the syntax that allows
to provide a parent structure and some extra fields.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">Ring&#8323;</span> <span class="o">(</span><span class="n">R</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">AddGroup&#8323;</span> <span class="n">R</span><span class="o">,</span> <span class="n">Monoid&#8323;</span> <span class="n">R</span><span class="o">,</span> <span class="n">MulZeroClass</span> <span class="n">R</span> <span class="n">where</span>
  <span class="sd">/-- Multiplication is left distributive over addition -/</span>
  <span class="n">left_distrib</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">R</span><span class="o">,</span> <span class="n">a</span> <span class="bp">*</span> <span class="o">(</span><span class="n">b</span> <span class="bp">+</span> <span class="n">c</span><span class="o">)</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">c</span>
  <span class="sd">/-- Multiplication is right distributive over addition -/</span>
  <span class="n">right_distrib</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">R</span><span class="o">,</span> <span class="o">(</span><span class="n">a</span> <span class="bp">+</span> <span class="n">b</span><span class="o">)</span> <span class="bp">*</span> <span class="n">c</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">c</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">*</span> <span class="n">c</span>

<span class="kd">instance</span> <span class="o">{</span><span class="n">R</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">}</span> <span class="o">[</span><span class="n">Ring&#8323;</span> <span class="n">R</span><span class="o">]</span> <span class="o">:</span> <span class="n">AddCommGroup&#8323;</span> <span class="n">R</span> <span class="o">:=</span>
<span class="o">{</span> <span class="n">Ring&#8323;.toAddGroup&#8323;</span> <span class="k">with</span>
  <span class="n">add_comm</span> <span class="o">:=</span> <span class="kd">by</span>
    <span class="gr">sorry</span> <span class="o">}</span>
</pre></div>
</div>
<p>Of course we can also build concrete instances, such as a ring structure on integers (of course
the instance below uses that all the work is already done in Mathlib).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span> <span class="o">:</span> <span class="n">Ring&#8323;</span> <span class="n">&#8484;</span> <span class="n">where</span>
  <span class="n">add</span> <span class="o">:=</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">+</span> <span class="bp">&#183;</span><span class="o">)</span>
  <span class="n">add_assoc&#8323;</span> <span class="o">:=</span> <span class="n">add_assoc</span>
  <span class="n">zero</span> <span class="o">:=</span> <span class="mi">0</span>
  <span class="n">zero_add</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">simp</span>
  <span class="n">add_zero</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">simp</span>
  <span class="n">neg</span> <span class="o">:=</span> <span class="o">(</span><span class="bp">-</span> <span class="bp">&#183;</span><span class="o">)</span>
  <span class="n">neg_add</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">simp</span>
  <span class="n">mul</span> <span class="o">:=</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">*</span> <span class="bp">&#183;</span><span class="o">)</span>
  <span class="n">mul_assoc&#8323;</span> <span class="o">:=</span> <span class="n">mul_assoc</span>
  <span class="n">one</span> <span class="o">:=</span> <span class="mi">1</span>
  <span class="n">one_mul</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">simp</span>
  <span class="n">mul_one</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">simp</span>
  <span class="n">zero_mul</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">simp</span>
  <span class="n">mul_zero</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">simp</span>
  <span class="n">left_distrib</span> <span class="o">:=</span> <span class="n">Int.mul_add</span>
  <span class="n">right_distrib</span> <span class="o">:=</span> <span class="n">Int.add_mul</span>
</pre></div>
</div>
<p>As an exercise you can now set up a simple hierarchy for order relations, including a class
for ordered commutative monoids, which have both a partial order and a commutative monoid structure
such that <code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">a</span> <span class="pre">b</span> <span class="pre">:</span> <span class="pre">&#945;,</span> <span class="pre">a</span> <span class="pre">&#8804;</span> <span class="pre">b</span> <span class="pre">&#8594;</span> <span class="pre">&#8704;</span> <span class="pre">c</span> <span class="pre">:</span> <span class="pre">&#945;,</span> <span class="pre">c</span> <span class="pre">*</span> <span class="pre">a</span> <span class="pre">&#8804;</span> <span class="pre">c</span> <span class="pre">*</span> <span class="pre">b</span></code>. Of course you need to add fields and maybe
<code class="docutils literal notranslate"><span class="pre">extends</span></code> clauses to the following classes.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">LE&#8321;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="n">where</span>
  <span class="sd">/-- The Less-or-Equal relation. -/</span>
  <span class="n">le</span> <span class="o">:</span> <span class="n">&#945;</span> <span class="bp">&#8594;</span> <span class="n">&#945;</span> <span class="bp">&#8594;</span> <span class="kt">Prop</span>

<span class="kd">@[inherit_doc]</span> <span class="kd">infix</span><span class="o">:</span><span class="mi">50</span> <span class="s2">&quot; &#8804;&#8321; &quot;</span> <span class="bp">=&gt;</span> <span class="n">LE&#8321;.le</span>

<span class="kd">class</span> <span class="n">Preorder&#8321;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span>

<span class="kd">class</span> <span class="n">PartialOrder&#8321;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span>

<span class="kd">class</span> <span class="n">OrderedCommMonoid&#8321;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span>

<span class="kd">instance</span> <span class="o">:</span> <span class="n">OrderedCommMonoid&#8321;</span> <span class="n">&#8469;</span> <span class="n">where</span>
</pre></div>
</div>
<p>We now want to discuss algebraic structures involving several types. The prime example
is modules over rings. If you don&#8217;t know what is a module, you can pretend it means vector space
and think that all our rings are fields. Those structures are commutative additive groups
equipped with a scalar multiplication by elements of some ring.</p>
<p>We first define the data-carrying type class of scalar multiplication by some type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> on some
type <code class="docutils literal notranslate"><span class="pre">&#946;</span></code>, and give it a right associative notation.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">SMul&#8323;</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">(</span><span class="n">&#946;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="n">where</span>
  <span class="sd">/-- Scalar multiplication -/</span>
  <span class="n">smul</span> <span class="o">:</span> <span class="n">&#945;</span> <span class="bp">&#8594;</span> <span class="n">&#946;</span> <span class="bp">&#8594;</span> <span class="n">&#946;</span>

<span class="kd">infixr</span><span class="o">:</span><span class="mi">73</span> <span class="s2">&quot; &#8226; &quot;</span> <span class="bp">=&gt;</span> <span class="n">SMul&#8323;.smul</span>
</pre></div>
</div>
<p>Then we can define modules (again think about vector spaces if you don&#8217;t know what is a module).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">Module&#8321;</span> <span class="o">(</span><span class="n">R</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">Ring&#8323;</span> <span class="n">R</span><span class="o">]</span> <span class="o">(</span><span class="n">M</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">AddCommGroup&#8323;</span> <span class="n">M</span><span class="o">]</span> <span class="kd">extends</span> <span class="n">SMul&#8323;</span> <span class="n">R</span> <span class="n">M</span> <span class="n">where</span>
  <span class="n">zero_smul</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">m</span> <span class="o">:</span> <span class="n">M</span><span class="o">,</span> <span class="o">(</span><span class="mi">0</span> <span class="o">:</span> <span class="n">R</span><span class="o">)</span> <span class="bp">&#8226;</span> <span class="n">m</span> <span class="bp">=</span> <span class="mi">0</span>
  <span class="n">one_smul</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">m</span> <span class="o">:</span> <span class="n">M</span><span class="o">,</span> <span class="o">(</span><span class="mi">1</span> <span class="o">:</span> <span class="n">R</span><span class="o">)</span> <span class="bp">&#8226;</span> <span class="n">m</span> <span class="bp">=</span> <span class="n">m</span>
  <span class="n">mul_smul</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">R</span><span class="o">)</span> <span class="o">(</span><span class="n">m</span> <span class="o">:</span> <span class="n">M</span><span class="o">),</span> <span class="o">(</span><span class="n">a</span> <span class="bp">*</span> <span class="n">b</span><span class="o">)</span> <span class="bp">&#8226;</span> <span class="n">m</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">&#8226;</span> <span class="n">b</span> <span class="bp">&#8226;</span> <span class="n">m</span>
  <span class="n">add_smul</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">R</span><span class="o">)</span> <span class="o">(</span><span class="n">m</span> <span class="o">:</span> <span class="n">M</span><span class="o">),</span> <span class="o">(</span><span class="n">a</span> <span class="bp">+</span> <span class="n">b</span><span class="o">)</span> <span class="bp">&#8226;</span> <span class="n">m</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">&#8226;</span> <span class="n">m</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">&#8226;</span> <span class="n">m</span>
  <span class="n">smul_add</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">a</span> <span class="o">:</span> <span class="n">R</span><span class="o">)</span> <span class="o">(</span><span class="n">m</span> <span class="n">n</span> <span class="o">:</span> <span class="n">M</span><span class="o">),</span> <span class="n">a</span> <span class="bp">&#8226;</span> <span class="o">(</span><span class="n">m</span> <span class="bp">+</span> <span class="n">n</span><span class="o">)</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">&#8226;</span> <span class="n">m</span> <span class="bp">+</span> <span class="n">a</span> <span class="bp">&#8226;</span> <span class="n">n</span>
</pre></div>
</div>
<p>There is something interesting going on here. While it isn&#8217;t too surprising that the
ring structure on <code class="docutils literal notranslate"><span class="pre">R</span></code> is a parameter in this definition, you probably expected <code class="docutils literal notranslate"><span class="pre">AddCommGroup&#8323;</span> <span class="pre">M</span></code>
to be part of the <code class="docutils literal notranslate"><span class="pre">extends</span></code> clause just as <code class="docutils literal notranslate"><span class="pre">SMul&#8323;</span> <span class="pre">R</span> <span class="pre">M</span></code> is.  Trying to do that would lead
to a mysterious sounding error message:
<code class="docutils literal notranslate"><span class="pre">cannot</span> <span class="pre">find</span> <span class="pre">synthesization</span> <span class="pre">order</span> <span class="pre">for</span> <span class="pre">instance</span> <span class="pre">Module&#8321;.toAddCommGroup&#8323;</span> <span class="pre">with</span> <span class="pre">type</span> <span class="pre">(R</span> <span class="pre">:</span> <span class="pre">Type)</span> <span class="pre">&#8594;</span> <span class="pre">[inst</span> <span class="pre">:</span> <span class="pre">Ring&#8323;</span> <span class="pre">R]</span> <span class="pre">&#8594;</span> <span class="pre">{M</span> <span class="pre">:</span> <span class="pre">Type}</span> <span class="pre">&#8594;</span> <span class="pre">[self</span> <span class="pre">:</span> <span class="pre">Module&#8321;</span> <span class="pre">R</span> <span class="pre">M]</span> <span class="pre">&#8594;</span> <span class="pre">AddCommGroup&#8323;</span> <span class="pre">M</span>
<span class="pre">all</span> <span class="pre">remaining</span> <span class="pre">arguments</span> <span class="pre">have</span> <span class="pre">metavariables:</span> <span class="pre">Ring&#8323;</span> <span class="pre">?R</span> <span class="pre">&#64;Module&#8321;</span> <span class="pre">?R</span> <span class="pre">?inst&#10013;</span> <span class="pre">M</span></code>.
In order to understand this message, you need to remember that such an <code class="docutils literal notranslate"><span class="pre">extends</span></code> clause would
lead to a field <code class="docutils literal notranslate"><span class="pre">Module&#8323;.toAddCommGroup&#8323;</span></code> marked as an instance. This instance
would have the signature appearing in the error message:
<code class="docutils literal notranslate"><span class="pre">(R</span> <span class="pre">:</span> <span class="pre">Type)</span> <span class="pre">&#8594;</span> <span class="pre">[inst</span> <span class="pre">:</span> <span class="pre">Ring&#8323;</span> <span class="pre">R]</span> <span class="pre">&#8594;</span> <span class="pre">{M</span> <span class="pre">:</span> <span class="pre">Type}</span> <span class="pre">&#8594;</span> <span class="pre">[self</span> <span class="pre">:</span> <span class="pre">Module&#8321;</span> <span class="pre">R</span> <span class="pre">M]</span> <span class="pre">&#8594;</span> <span class="pre">AddCommGroup&#8323;</span> <span class="pre">M</span></code>.
With such an instance in the type class database, each time Lean would look for a
<code class="docutils literal notranslate"><span class="pre">AddCommGroup&#8323;</span> <span class="pre">M</span></code> instance for some <code class="docutils literal notranslate"><span class="pre">M</span></code>, it would need to go hunting for a completely
unspecified type <code class="docutils literal notranslate"><span class="pre">R</span></code> and a <code class="docutils literal notranslate"><span class="pre">Ring&#8323;</span> <span class="pre">R</span></code> instance before embarking on the main quest of finding a
<code class="docutils literal notranslate"><span class="pre">Module&#8321;</span> <span class="pre">R</span> <span class="pre">M</span></code> instance. Those two side-quests are represented by the meta-variables mentioned in
the error message and denoted by <code class="docutils literal notranslate"><span class="pre">?R</span></code> and <code class="docutils literal notranslate"><span class="pre">?inst&#10013;</span></code> there. Such a <code class="docutils literal notranslate"><span class="pre">Module&#8323;.toAddCommGroup&#8323;</span></code>
instance would then be a huge trap for the instance resolution procedure and then <code class="docutils literal notranslate"><span class="pre">class</span></code> command
refuses to set it up.</p>
<p>What about <code class="docutils literal notranslate"><span class="pre">extends</span> <span class="pre">SMul&#8323;</span> <span class="pre">R</span> <span class="pre">M</span></code> then? That one creates a field
<code class="docutils literal notranslate"><span class="pre">Module&#8321;.toSMul&#8323;</span> <span class="pre">:</span> <span class="pre">{R</span> <span class="pre">:</span> <span class="pre">Type}</span> <span class="pre">&#8594;</span>&#160; <span class="pre">[inst</span> <span class="pre">:</span> <span class="pre">Ring&#8323;</span> <span class="pre">R]</span> <span class="pre">&#8594;</span> <span class="pre">{M</span> <span class="pre">:</span> <span class="pre">Type}</span> <span class="pre">&#8594;</span> <span class="pre">[inst_1</span> <span class="pre">:</span> <span class="pre">AddCommGroup&#8323;</span> <span class="pre">M]</span> <span class="pre">&#8594;</span> <span class="pre">[self</span> <span class="pre">:</span> <span class="pre">Module&#8321;</span> <span class="pre">R</span> <span class="pre">M]</span> <span class="pre">&#8594;</span> <span class="pre">SMul&#8323;</span> <span class="pre">R</span> <span class="pre">M</span></code>
whose end result <code class="docutils literal notranslate"><span class="pre">SMul&#8323;</span> <span class="pre">R</span> <span class="pre">M</span></code> mentions both <code class="docutils literal notranslate"><span class="pre">R</span></code> and <code class="docutils literal notranslate"><span class="pre">M</span></code> so this field can
safely be used as an instance. The rule is easy to remember: each class appearing in the
<code class="docutils literal notranslate"><span class="pre">extends</span></code> clause should mention every type appearing in the parameters.</p>
<p>Let us create our first module instance: a ring is a module over itself using its multiplication
as a scalar multiplication.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span> <span class="n">selfModule</span> <span class="o">(</span><span class="n">R</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">Ring&#8323;</span> <span class="n">R</span><span class="o">]</span> <span class="o">:</span> <span class="n">Module&#8321;</span> <span class="n">R</span> <span class="n">R</span> <span class="n">where</span>
  <span class="n">smul</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">r</span> <span class="n">s</span> <span class="bp">&#8614;</span> <span class="n">r</span><span class="bp">*</span><span class="n">s</span>
  <span class="n">zero_smul</span> <span class="o">:=</span> <span class="n">zero_mul</span>
  <span class="n">one_smul</span> <span class="o">:=</span> <span class="n">one_mul</span>
  <span class="n">mul_smul</span> <span class="o">:=</span> <span class="n">mul_assoc&#8323;</span>
  <span class="n">add_smul</span> <span class="o">:=</span> <span class="n">Ring&#8323;.right_distrib</span>
  <span class="n">smul_add</span> <span class="o">:=</span> <span class="n">Ring&#8323;.left_distrib</span>
</pre></div>
</div>
<p>As a second example, every abelian group is a module over <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code> (this is one of the reason to
generalize the theory of vector spaces by allowing non-invertible scalars). First one can define
scalar multiplication by a natural number for any type equipped with a zero and an addition:
<code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">&#8226;</span> <span class="pre">a</span></code> is defined as <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">+</span> <span class="pre">&#8943;</span> <span class="pre">+</span> <span class="pre">a</span></code> where <code class="docutils literal notranslate"><span class="pre">a</span></code> appears <code class="docutils literal notranslate"><span class="pre">n</span></code> times. Then this is extended
to scalar multiplication by an integer by ensuring <code class="docutils literal notranslate"><span class="pre">(-1)</span> <span class="pre">&#8226;</span> <span class="pre">a</span> <span class="pre">=</span> <span class="pre">-a</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">nsmul&#8321;</span> <span class="o">[</span><span class="n">Zero</span> <span class="n">M</span><span class="o">]</span> <span class="o">[</span><span class="n">Add</span> <span class="n">M</span><span class="o">]</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">M</span> <span class="bp">&#8594;</span> <span class="n">M</span>
  <span class="bp">|</span> <span class="mi">0</span><span class="o">,</span> <span class="n">_</span> <span class="bp">=&gt;</span> <span class="mi">0</span>
  <span class="bp">|</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">,</span> <span class="n">a</span> <span class="bp">=&gt;</span> <span class="n">a</span> <span class="bp">+</span> <span class="n">nsmul&#8321;</span> <span class="n">n</span> <span class="n">a</span>

<span class="kd">def</span> <span class="n">zsmul&#8321;</span> <span class="o">{</span><span class="n">M</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">Zero</span> <span class="n">M</span><span class="o">]</span> <span class="o">[</span><span class="n">Add</span> <span class="n">M</span><span class="o">]</span> <span class="o">[</span><span class="n">Neg</span> <span class="n">M</span><span class="o">]</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">&#8594;</span> <span class="n">M</span> <span class="bp">&#8594;</span> <span class="n">M</span>
  <span class="bp">|</span> <span class="n">Int.ofNat</span> <span class="n">n</span><span class="o">,</span> <span class="n">a</span> <span class="bp">=&gt;</span> <span class="n">nsmul&#8321;</span> <span class="n">n</span> <span class="n">a</span>
  <span class="bp">|</span> <span class="n">Int.negSucc</span> <span class="n">n</span><span class="o">,</span> <span class="n">a</span> <span class="bp">=&gt;</span> <span class="bp">-</span><span class="n">nsmul&#8321;</span> <span class="n">n.succ</span> <span class="n">a</span>
</pre></div>
</div>
<p>Proving this gives rise to a module structure is a bit tedious and not interesting for the
current discussion, so we will sorry all axioms. You are <em>not</em> asked to replace those sorries
with proofs. If you insist on doing it then you will probably want to state and prove several
intermediate lemmas about <code class="docutils literal notranslate"><span class="pre">nsmul&#8321;</span></code> and <code class="docutils literal notranslate"><span class="pre">zsmul&#8321;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span> <span class="n">abGrpModule</span> <span class="o">(</span><span class="n">A</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">AddCommGroup&#8323;</span> <span class="n">A</span><span class="o">]</span> <span class="o">:</span> <span class="n">Module&#8321;</span> <span class="n">&#8484;</span> <span class="n">A</span> <span class="n">where</span>
  <span class="n">smul</span> <span class="o">:=</span> <span class="n">zsmul&#8321;</span>
  <span class="n">zero_smul</span> <span class="o">:=</span> <span class="gr">sorry</span>
  <span class="n">one_smul</span> <span class="o">:=</span> <span class="gr">sorry</span>
  <span class="n">mul_smul</span> <span class="o">:=</span> <span class="gr">sorry</span>
  <span class="n">add_smul</span> <span class="o">:=</span> <span class="gr">sorry</span>
  <span class="n">smul_add</span> <span class="o">:=</span> <span class="gr">sorry</span>
</pre></div>
</div>
<p>A much more important issue is that we now have two module structures over the ring <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code>
for <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code> itself: <code class="docutils literal notranslate"><span class="pre">abGrpModule</span> <span class="pre">&#8484;</span></code> since <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code> is a abelian group, and <code class="docutils literal notranslate"><span class="pre">selfModule</span> <span class="pre">&#8484;</span></code> since
<code class="docutils literal notranslate"><span class="pre">&#8484;</span></code> is a ring. Those two module structure correspond to the same abelian group structure,
but it is not obvious that they have the same scalar multiplication. They actually do, but
this isn&#8217;t true by definition, it requires a proof. This is very bad news for the type class
instance resolution procedure and will lead to very frustrating failures for users of this
hierarchy. When directly asked to find an instance, Lean will pick one, and we can see
which one using:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="bp">#</span><span class="n">synth</span> <span class="n">Module&#8321;</span> <span class="n">&#8484;</span> <span class="n">&#8484;</span> <span class="c1">-- abGrpModule &#8484;</span>
</pre></div>
</div>
<p>But in a more indirect context it can happen that Lean infers the one and then gets confused.
This situation is known as a bad diamond. This has nothing to do with the diamond operation
we used above, it refers to the way one can draw the paths from <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code> to its <code class="docutils literal notranslate"><span class="pre">Module&#8321;</span> <span class="pre">&#8484;</span></code>
going through either <code class="docutils literal notranslate"><span class="pre">AddCommGroup&#8323;</span> <span class="pre">&#8484;</span></code> or <code class="docutils literal notranslate"><span class="pre">Ring&#8323;</span> <span class="pre">&#8484;</span></code>.</p>
<p>It is important to understand that not all diamonds are bad. In fact there are diamonds everywhere
in Mathlib, and also in this chapter. Already at the very beginning we saw one can go
from <code class="docutils literal notranslate"><span class="pre">Monoid&#8321;</span> <span class="pre">&#945;</span></code> to <code class="docutils literal notranslate"><span class="pre">Dia&#8321;</span> <span class="pre">&#945;</span></code> through either <code class="docutils literal notranslate"><span class="pre">Semigroup&#8321;</span> <span class="pre">&#945;</span></code> or <code class="docutils literal notranslate"><span class="pre">DiaOneClass&#8321;</span> <span class="pre">&#945;</span></code> and
thanks to the work done by the <code class="docutils literal notranslate"><span class="pre">class</span></code> command, the resulting two <code class="docutils literal notranslate"><span class="pre">Dia&#8321;</span> <span class="pre">&#945;</span></code> instances
are definitionally equal. In particular a diamond having a <code class="docutils literal notranslate"><span class="pre">Prop</span></code>-valued class at the bottom
cannot be bad since any too proofs of the same statement are definitionally equal.</p>
<p>But the diamond we created with modules is definitely bad. The offending piece is the <code class="docutils literal notranslate"><span class="pre">smul</span></code>
field which is data, not a proof, and we have two constructions that are not definitionally equal.
The robust way of fixing this issue is to make sure that going from a rich structure to a
poor structure is always done by forgetting data, not by defining data. This well-known pattern
as been named &#8220;forgetful inheritance&#8221; and extensively discussed in
<a class="reference external" href="https://inria.hal.science/hal-02463336">https://inria.hal.science/hal-02463336</a>.</p>
<p>In our concrete case, we can modify the definition of <code class="docutils literal notranslate"><span class="pre">AddMonoid&#8323;</span></code> to include a <code class="docutils literal notranslate"><span class="pre">nsmul</span></code> data
field and some <code class="docutils literal notranslate"><span class="pre">Prop</span></code>-valued fields ensuring this operation is provably the one we constructed
above. Those fields are given default values using <code class="docutils literal notranslate"><span class="pre">:=</span></code> after their type in the definition below.
Thanks to these default values, most instances would be constructed exactly as with our previous
definitions. But in the special case of <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code> we will be able to provide specific values.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">AddMonoid&#8324;</span> <span class="o">(</span><span class="n">M</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="kd">extends</span> <span class="n">AddSemigroup&#8323;</span> <span class="n">M</span><span class="o">,</span> <span class="n">AddZeroClass</span> <span class="n">M</span> <span class="n">where</span>
  <span class="sd">/-- Multiplication by a natural number. -/</span>
  <span class="n">nsmul</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">M</span> <span class="bp">&#8594;</span> <span class="n">M</span> <span class="o">:=</span> <span class="n">nsmul&#8321;</span>
  <span class="sd">/-- Multiplication by `(0 : &#8469;)` gives `0`. -/</span>
  <span class="n">nsmul_zero</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">x</span><span class="o">,</span> <span class="n">nsmul</span> <span class="mi">0</span> <span class="n">x</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">intros</span><span class="bp">;</span> <span class="n">rfl</span>
  <span class="sd">/-- Multiplication by `(n + 1 : &#8469;)` behaves as expected. -/</span>
  <span class="n">nsmul_succ</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">(</span><span class="n">x</span><span class="o">),</span> <span class="n">nsmul</span> <span class="o">(</span><span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="n">x</span> <span class="bp">=</span> <span class="n">x</span> <span class="bp">+</span> <span class="n">nsmul</span> <span class="n">n</span> <span class="n">x</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">intros</span><span class="bp">;</span> <span class="n">rfl</span>

<span class="kd">instance</span> <span class="n">mySMul</span> <span class="o">{</span><span class="n">M</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">}</span> <span class="o">[</span><span class="n">AddMonoid&#8324;</span> <span class="n">M</span><span class="o">]</span> <span class="o">:</span> <span class="n">SMul</span> <span class="n">&#8469;</span> <span class="n">M</span> <span class="o">:=</span> <span class="o">&#10216;</span><span class="n">AddMonoid&#8324;.nsmul</span><span class="o">&#10217;</span>
</pre></div>
</div>
<p>Let us check we can still construct a product monoid instance without providing the <code class="docutils literal notranslate"><span class="pre">nsmul</span></code>
related fields.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span> <span class="o">(</span><span class="n">M</span> <span class="n">N</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">AddMonoid&#8324;</span> <span class="n">M</span><span class="o">]</span> <span class="o">[</span><span class="n">AddMonoid&#8324;</span> <span class="n">N</span><span class="o">]</span> <span class="o">:</span> <span class="n">AddMonoid&#8324;</span> <span class="o">(</span><span class="n">M</span> <span class="bp">&#215;</span> <span class="n">N</span><span class="o">)</span> <span class="n">where</span>
  <span class="n">add</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">p</span> <span class="n">q</span> <span class="bp">&#8614;</span> <span class="o">(</span><span class="n">p.1</span> <span class="bp">+</span> <span class="n">q.1</span><span class="o">,</span> <span class="n">p.2</span> <span class="bp">+</span> <span class="n">q.2</span><span class="o">)</span>
  <span class="n">add_assoc&#8323;</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="bp">&#8614;</span> <span class="kd">by</span> <span class="n">ext</span> <span class="bp">&lt;;&gt;</span> <span class="n">apply</span> <span class="n">add_assoc&#8323;</span>
  <span class="n">zero</span> <span class="o">:=</span> <span class="o">(</span><span class="mi">0</span><span class="o">,</span> <span class="mi">0</span><span class="o">)</span>
  <span class="n">zero_add</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">a</span> <span class="bp">&#8614;</span> <span class="kd">by</span> <span class="n">ext</span> <span class="bp">&lt;;&gt;</span> <span class="n">apply</span> <span class="n">zero_add</span>
  <span class="n">add_zero</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">a</span> <span class="bp">&#8614;</span> <span class="kd">by</span> <span class="n">ext</span> <span class="bp">&lt;;&gt;</span> <span class="n">apply</span> <span class="n">add_zero</span>
</pre></div>
</div>
<p>And now let us handle the special case of <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code> where we want to build <code class="docutils literal notranslate"><span class="pre">nsmul</span></code> using the coercion
of <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code> to <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code> and the multiplication on <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code>. Note in particular how the proof fields
contain more work than in the default value above.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span> <span class="o">:</span> <span class="n">AddMonoid&#8324;</span> <span class="n">&#8484;</span> <span class="n">where</span>
  <span class="n">add</span> <span class="o">:=</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">+</span> <span class="bp">&#183;</span><span class="o">)</span>
  <span class="n">add_assoc&#8323;</span> <span class="o">:=</span> <span class="n">Int.add_assoc</span>
  <span class="n">zero</span> <span class="o">:=</span> <span class="mi">0</span>
  <span class="n">zero_add</span> <span class="o">:=</span> <span class="n">Int.zero_add</span>
  <span class="n">add_zero</span> <span class="o">:=</span> <span class="n">Int.add_zero</span>
  <span class="n">nsmul</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">n</span> <span class="n">m</span> <span class="bp">&#8614;</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">*</span> <span class="n">m</span>
  <span class="n">nsmul_zero</span> <span class="o">:=</span> <span class="n">Int.zero_mul</span>
  <span class="n">nsmul_succ</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">n</span> <span class="n">m</span> <span class="bp">&#8614;</span> <span class="k">show</span> <span class="o">(</span><span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">*</span> <span class="n">m</span> <span class="bp">=</span> <span class="n">m</span> <span class="bp">+</span> <span class="n">n</span> <span class="bp">*</span> <span class="n">m</span>
    <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">Int.add_mul</span><span class="o">,</span> <span class="n">Int.add_comm</span><span class="o">,</span> <span class="n">Int.one_mul</span><span class="o">]</span>
</pre></div>
</div>
<p>Let us check we solved our issue. Because Lean already has a definition of scalar multiplication
of a natural number and an integer, and we want to make sure our instance is used, we won&#8217;t use
the <code class="docutils literal notranslate"><span class="pre">&#8226;</span></code> notation but call <code class="docutils literal notranslate"><span class="pre">SMul.mul</span></code> and explicitly provide our instance defined above.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">(</span><span class="n">m</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">SMul.smul</span> <span class="o">(</span><span class="n">self</span> <span class="o">:=</span> <span class="n">mySMul</span><span class="o">)</span> <span class="n">n</span> <span class="n">m</span> <span class="bp">=</span> <span class="n">n</span> <span class="bp">*</span> <span class="n">m</span> <span class="o">:=</span> <span class="n">rfl</span>
</pre></div>
</div>
<p>This story then continues with incorporating a <code class="docutils literal notranslate"><span class="pre">zsmul</span></code> field into the definition of groups
and similar tricks. You are now ready to read the definition of monoids, groups, rings and modules
in Mathlib. There are more complicated than what we have seen here, because they are part of a huge
hierarchy, but all principles have been explained above.</p>
<p>As an exercise, you can come back to the order relation hierarchy you built above and try
to incorporate a type class <code class="docutils literal notranslate"><span class="pre">LT&#8321;</span></code> carrying the Less-Than notation <code class="docutils literal notranslate"><span class="pre">&lt;&#8321;</span></code> and make sure
that every preorder comes with a <code class="docutils literal notranslate"><span class="pre">&lt;&#8321;</span></code> which has a default value built from <code class="docutils literal notranslate"><span class="pre">&#8804;&#8321;</span></code> and a
<code class="docutils literal notranslate"><span class="pre">Prop</span></code>-valued field asserting the natural relation between those two comparison operators.
-/</p>
</div>
<div class="section" id="morphisms">
<span id="section-hierarchies-morphisms"></span><h2><span class="section-number">7.2. </span>Morphisms<a class="headerlink" href="#morphisms" title="Permalink to this headline">&#61633;</a></h2>
<p>So far in this chapter, we discussed how to create a hierarchy of mathematical structures.
But defining structures is not really completed until we have morphisms. There are two
main approaches here. The most obvious one is to define a predicate on functions.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">isMonoidHom&#8321;</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">G</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">H</span><span class="o">]</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">G</span> <span class="bp">&#8594;</span> <span class="n">H</span><span class="o">)</span> <span class="o">:</span> <span class="kt">Prop</span> <span class="o">:=</span>
  <span class="n">f</span> <span class="mi">1</span> <span class="bp">=</span> <span class="mi">1</span> <span class="bp">&#8743;</span> <span class="bp">&#8704;</span> <span class="n">g</span> <span class="n">g&#39;</span><span class="o">,</span> <span class="n">f</span> <span class="o">(</span><span class="n">g</span> <span class="bp">*</span> <span class="n">g&#39;</span><span class="o">)</span> <span class="bp">=</span> <span class="n">f</span> <span class="n">g</span> <span class="bp">*</span> <span class="n">f</span> <span class="n">g&#39;</span>
</pre></div>
</div>
<p>In this definition, it is a bit unpleasant to use a conjunction. In particular users
will need to remember the ordering we chose when they want to access the two conditions.
So we could use a structure instead.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">structure</span> <span class="n">isMonoidHom&#8322;</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">G</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">H</span><span class="o">]</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">G</span> <span class="bp">&#8594;</span> <span class="n">H</span><span class="o">)</span> <span class="o">:</span> <span class="kt">Prop</span> <span class="n">where</span>
  <span class="n">map_one</span> <span class="o">:</span> <span class="n">f</span> <span class="mi">1</span> <span class="bp">=</span> <span class="mi">1</span>
  <span class="n">map_mul</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">g</span> <span class="n">g&#39;</span><span class="o">,</span> <span class="n">f</span> <span class="o">(</span><span class="n">g</span> <span class="bp">*</span> <span class="n">g&#39;</span><span class="o">)</span> <span class="bp">=</span> <span class="n">f</span> <span class="n">g</span> <span class="bp">*</span> <span class="n">f</span> <span class="n">g&#39;</span>
</pre></div>
</div>
<p>Once we are here, it is even tempting to make it a class and use the type class instance resolution
procedure to automatically infer <code class="docutils literal notranslate"><span class="pre">isMonoidHom&#8322;</span></code> for complicated functions out of instances for
simpler functions. For instance a composition of monoid morphisms is a monoid morphism and this
seems like a useful instance. However such an instance would be very tricky for the resolution
procedure since it would need to hunt down <code class="docutils literal notranslate"><span class="pre">g</span> <span class="pre">&#8728;</span> <span class="pre">f</span></code> everywhere. Seeing it failing in <code class="docutils literal notranslate"><span class="pre">g</span> <span class="pre">(f</span> <span class="pre">x)</span></code>
would be very frustrating. More generally one must always keep in mind that recognizing which
function is applied in a given expression is a very difficult problem, called the &#8220;higher-order
unification problem&#8221;. So Mathlib does not use this class approach.</p>
<p>A more fundamental question is whether we use predicates as above (using either a <code class="docutils literal notranslate"><span class="pre">def</span></code> or a
<code class="docutils literal notranslate"><span class="pre">structure</span></code>) or use structures bundling a function and predicates. This is partly a psychological
issue. It is extremely rare to consider a function between monoids that is not a morphism.
It really feels like &#8220;monoid morphism&#8221; is not an adjective you can assign to a bare function,
it is a noun. On the other hand one can argue that a continuous function between topological spaces
is really a function that happens to be continuous. This is one reason why Mathlib has a
<code class="docutils literal notranslate"><span class="pre">Continuous</span></code> predicate. For instance you can write:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Continuous</span> <span class="o">(</span><span class="n">id</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">&#8594;</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:=</span> <span class="n">continuous_id</span>
</pre></div>
</div>
<p>We still have bundles continuous functions, which are convenient for instance to put a topology
on a space of continuous functions, but they are not the primary tool to work with continuity.</p>
<p>By contrast, morphisms between monoids (or other algebraic structures) are bundled as in:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[ext]</span>
<span class="kd">structure</span> <span class="n">MonoidHom&#8321;</span> <span class="o">(</span><span class="n">G</span> <span class="n">H</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">G</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">H</span><span class="o">]</span>  <span class="n">where</span>
  <span class="n">toFun</span> <span class="o">:</span> <span class="n">G</span> <span class="bp">&#8594;</span> <span class="n">H</span>
  <span class="n">map_one</span> <span class="o">:</span> <span class="n">toFun</span> <span class="mi">1</span> <span class="bp">=</span> <span class="mi">1</span>
  <span class="n">map_mul</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">g</span> <span class="n">g&#39;</span><span class="o">,</span> <span class="n">toFun</span> <span class="o">(</span><span class="n">g</span> <span class="bp">*</span> <span class="n">g&#39;</span><span class="o">)</span> <span class="bp">=</span> <span class="n">toFun</span> <span class="n">g</span> <span class="bp">*</span> <span class="n">toFun</span> <span class="n">g&#39;</span>
</pre></div>
</div>
<p>Of course we don&#8217;t want to type <code class="docutils literal notranslate"><span class="pre">toFun</span></code> everywhere so we register a coercion using
the <code class="docutils literal notranslate"><span class="pre">CoeFun</span></code> type class. Its first argument is the type we want to coerce to a function.
The second argument describes the target function type. In our case it is always <code class="docutils literal notranslate"><span class="pre">G</span> <span class="pre">&#8594;</span> <span class="pre">H</span></code>
for every <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">MonoidHom&#8321;</span> <span class="pre">G</span> <span class="pre">H</span></code>. We also tag <code class="docutils literal notranslate"><span class="pre">MonoidHom&#8321;.toFun</span></code> with the <code class="docutils literal notranslate"><span class="pre">coe</span></code> attribute to
make sure it is displayed almost invisibly in the tactic state, simply by a <code class="docutils literal notranslate"><span class="pre">&#8593;</span></code> prefix.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">G</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">H</span><span class="o">]</span> <span class="o">:</span> <span class="n">CoeFun</span> <span class="o">(</span><span class="n">MonoidHom&#8321;</span> <span class="n">G</span> <span class="n">H</span><span class="o">)</span> <span class="o">(</span><span class="k">fun</span> <span class="n">_</span> <span class="bp">&#8614;</span> <span class="n">G</span> <span class="bp">&#8594;</span> <span class="n">H</span><span class="o">)</span> <span class="n">where</span>
  <span class="n">coe</span> <span class="o">:=</span> <span class="n">MonoidHom&#8321;.toFun</span>

<span class="kn">attribute</span> <span class="o">[</span><span class="n">coe</span><span class="o">]</span> <span class="n">MonoidHom&#8321;.toFun</span>
</pre></div>
</div>
<p>Let us check we can indeed apply a bundled monoid morphism to an element.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">G</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">H</span><span class="o">]</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">MonoidHom&#8321;</span> <span class="n">G</span> <span class="n">H</span><span class="o">)</span> <span class="o">:</span> <span class="n">f</span> <span class="mi">1</span> <span class="bp">=</span> <span class="mi">1</span> <span class="o">:=</span>  <span class="n">f.map_one</span>
</pre></div>
</div>
<p>We can do the same with other kind of morphisms until we reach ring morphisms.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[ext]</span>
<span class="kd">structure</span> <span class="n">AddMonoidHom&#8321;</span> <span class="o">(</span><span class="n">G</span> <span class="n">H</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">AddMonoid</span> <span class="n">G</span><span class="o">]</span> <span class="o">[</span><span class="n">AddMonoid</span> <span class="n">H</span><span class="o">]</span>  <span class="n">where</span>
  <span class="n">toFun</span> <span class="o">:</span> <span class="n">G</span> <span class="bp">&#8594;</span> <span class="n">H</span>
  <span class="n">map_zero</span> <span class="o">:</span> <span class="n">toFun</span> <span class="mi">0</span> <span class="bp">=</span> <span class="mi">0</span>
  <span class="n">map_add</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">g</span> <span class="n">g&#39;</span><span class="o">,</span> <span class="n">toFun</span> <span class="o">(</span><span class="n">g</span> <span class="bp">+</span> <span class="n">g&#39;</span><span class="o">)</span> <span class="bp">=</span> <span class="n">toFun</span> <span class="n">g</span> <span class="bp">+</span> <span class="n">toFun</span> <span class="n">g&#39;</span>

<span class="kd">instance</span> <span class="o">[</span><span class="n">AddMonoid</span> <span class="n">G</span><span class="o">]</span> <span class="o">[</span><span class="n">AddMonoid</span> <span class="n">H</span><span class="o">]</span> <span class="o">:</span> <span class="n">CoeFun</span> <span class="o">(</span><span class="n">AddMonoidHom&#8321;</span> <span class="n">G</span> <span class="n">H</span><span class="o">)</span> <span class="o">(</span><span class="k">fun</span> <span class="n">_</span> <span class="bp">&#8614;</span> <span class="n">G</span> <span class="bp">&#8594;</span> <span class="n">H</span><span class="o">)</span> <span class="n">where</span>
  <span class="n">coe</span> <span class="o">:=</span> <span class="n">AddMonoidHom&#8321;.toFun</span>

<span class="kn">attribute</span> <span class="o">[</span><span class="n">coe</span><span class="o">]</span> <span class="n">AddMonoidHom&#8321;.toFun</span>

<span class="kd">@[ext]</span>
<span class="kd">structure</span> <span class="n">RingHom&#8321;</span> <span class="o">(</span><span class="n">R</span> <span class="n">S</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">Ring</span> <span class="n">R</span><span class="o">]</span> <span class="o">[</span><span class="n">Ring</span> <span class="n">S</span><span class="o">]</span> <span class="kd">extends</span> <span class="n">MonoidHom&#8321;</span> <span class="n">R</span> <span class="n">S</span><span class="o">,</span> <span class="n">AddMonoidHom&#8321;</span> <span class="n">R</span> <span class="n">S</span>
</pre></div>
</div>
<p>There are a couple of issues about this approach. A minor one is we don&#8217;t quite know where to put
the <code class="docutils literal notranslate"><span class="pre">coe</span></code> attribute since the <code class="docutils literal notranslate"><span class="pre">RingHom&#8321;.toFun</span></code> does not exist, the relevant function is
<code class="docutils literal notranslate"><span class="pre">MonoidHom&#8321;.toFun</span> <span class="pre">&#8728;</span> <span class="pre">RingHom&#8321;.toMonoidHom&#8321;</span></code> which is not a declaration that can be tagged with an
attribute (but we could still define a <code class="docutils literal notranslate"><span class="pre">CoeFun</span>&#160; <span class="pre">(RingHom&#8321;</span> <span class="pre">R</span> <span class="pre">S)</span> <span class="pre">(fun</span> <span class="pre">_</span> <span class="pre">&#8614;</span> <span class="pre">R</span> <span class="pre">&#8594;</span> <span class="pre">S)</span></code> instance).
A much more important one is that lemmas about monoid morphisms won&#8217;t directly apply
to ring morphisms. This leaves the alternative of either juggling with <code class="docutils literal notranslate"><span class="pre">RingHom&#8321;.toMonoidHom&#8321;</span></code>
each time we want to apply a monoid morphism lemma or restate every such lemmas for ring morphisms.
Neither option is appealing so Mathlib uses a new hierarchy trick here. The idea is to define
a type class for objects that are at least monoid morphisms, instantiate that class with both monoid
morphisms and ring morphisms and use it to state every lemma. In the definition below,
<code class="docutils literal notranslate"><span class="pre">F</span></code> could be <code class="docutils literal notranslate"><span class="pre">MonoidHom&#8321;</span> <span class="pre">M</span> <span class="pre">N</span></code>, or <code class="docutils literal notranslate"><span class="pre">RingHom&#8321;</span> <span class="pre">M</span> <span class="pre">N</span></code> if <code class="docutils literal notranslate"><span class="pre">M</span></code> and <code class="docutils literal notranslate"><span class="pre">N</span></code> have a ring structure.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">MonoidHomClass&#8321;</span> <span class="o">(</span><span class="n">F</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">(</span><span class="n">M</span> <span class="n">N</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">N</span><span class="o">]</span> <span class="n">where</span>
  <span class="n">toFun</span> <span class="o">:</span> <span class="n">F</span> <span class="bp">&#8594;</span> <span class="n">M</span> <span class="bp">&#8594;</span> <span class="n">N</span>
  <span class="n">map_one</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">f</span> <span class="o">:</span> <span class="n">F</span><span class="o">,</span> <span class="n">toFun</span> <span class="n">f</span> <span class="mi">1</span> <span class="bp">=</span> <span class="mi">1</span>
  <span class="n">map_mul</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">f</span> <span class="n">g</span> <span class="n">g&#39;</span><span class="o">,</span> <span class="n">toFun</span> <span class="n">f</span> <span class="o">(</span><span class="n">g</span> <span class="bp">*</span> <span class="n">g&#39;</span><span class="o">)</span> <span class="bp">=</span> <span class="n">toFun</span> <span class="n">f</span> <span class="n">g</span> <span class="bp">*</span> <span class="n">toFun</span> <span class="n">f</span> <span class="n">g&#39;</span>
</pre></div>
</div>
<p>However there is a problem with the above implementation. We haven&#8217;t registered a coercion to
function instance yet. Let us try to do it now.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">badInst</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">N</span><span class="o">]</span> <span class="o">[</span><span class="n">MonoidHomClass&#8321;</span> <span class="n">F</span> <span class="n">M</span> <span class="n">N</span><span class="o">]</span> <span class="o">:</span> <span class="n">CoeFun</span> <span class="n">F</span> <span class="o">(</span><span class="k">fun</span> <span class="n">_</span> <span class="bp">&#8614;</span> <span class="n">M</span> <span class="bp">&#8594;</span> <span class="n">N</span><span class="o">)</span> <span class="n">where</span>
  <span class="n">coe</span> <span class="o">:=</span> <span class="n">MonoidHomClass&#8321;.toFun</span>
</pre></div>
</div>
<p>Making this an instance would be bad. When faced with something like <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">x</span></code> where the type of <code class="docutils literal notranslate"><span class="pre">f</span></code>
is not a function type, Lean will try to find a <code class="docutils literal notranslate"><span class="pre">CoeFun</span></code> instance to coerce <code class="docutils literal notranslate"><span class="pre">f</span></code> into a function.
The above function has type:
<code class="docutils literal notranslate"><span class="pre">{M</span> <span class="pre">N</span> <span class="pre">F</span> <span class="pre">:</span> <span class="pre">Type}</span> <span class="pre">&#8594;</span> <span class="pre">[Monoid</span> <span class="pre">M]</span> <span class="pre">&#8594;</span> <span class="pre">[Monoid</span> <span class="pre">N]</span> <span class="pre">&#8594;</span> <span class="pre">[MonoidHomClass&#8321;</span> <span class="pre">F</span> <span class="pre">M</span> <span class="pre">N]</span> <span class="pre">&#8594;</span> <span class="pre">CoeFun</span> <span class="pre">F</span> <span class="pre">(fun</span> <span class="pre">x</span> <span class="pre">&#8614;</span> <span class="pre">M</span> <span class="pre">&#8594;</span> <span class="pre">N)</span></code>
so, when it trying to apply it, it wouldn&#8217;t be a priori clear to Lean in which order the unknown
types <code class="docutils literal notranslate"><span class="pre">M</span></code>, <code class="docutils literal notranslate"><span class="pre">N</span></code> and <code class="docutils literal notranslate"><span class="pre">F</span></code> should be inferred. This is a kind of bad instance that is slightly
different from the one we saw already, but it boils down to the same issue: without knowing <code class="docutils literal notranslate"><span class="pre">M</span></code>,
Lean would have to search for a monoid instance on an unknown type, hence hopelessly try <em>every</em>
monoid instance in the database. If you are curious to see the effect of such an instance you
can type <code class="docutils literal notranslate"><span class="pre">set_option</span> <span class="pre">synthInstance.checkSynthOrder</span> <span class="pre">false</span> <span class="pre">in</span></code> on top of the above declaration,
replace <code class="docutils literal notranslate"><span class="pre">def</span> <span class="pre">badInst</span></code> with <code class="docutils literal notranslate"><span class="pre">instance</span></code>, and look for random failures in this file.</p>
<p>Here the solution is easy, we need to tell Lean to first search what is <code class="docutils literal notranslate"><span class="pre">F</span></code> and then deduce <code class="docutils literal notranslate"><span class="pre">M</span></code>
and <code class="docutils literal notranslate"><span class="pre">N</span></code>. This is done using the <code class="docutils literal notranslate"><span class="pre">outParam</span></code> function. This function is defined as the identity
function, but is still recognized by the type class machinery and triggers the desired behavior.
Hence we can retry defining our class, paying attention to the <code class="docutils literal notranslate"><span class="pre">outParam</span></code> function:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">MonoidHomClass&#8322;</span> <span class="o">(</span><span class="n">F</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">(</span><span class="n">M</span> <span class="n">N</span> <span class="o">:</span> <span class="n">outParam</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">N</span><span class="o">]</span> <span class="n">where</span>
  <span class="n">toFun</span> <span class="o">:</span> <span class="n">F</span> <span class="bp">&#8594;</span> <span class="n">M</span> <span class="bp">&#8594;</span> <span class="n">N</span>
  <span class="n">map_one</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">f</span> <span class="o">:</span> <span class="n">F</span><span class="o">,</span> <span class="n">toFun</span> <span class="n">f</span> <span class="mi">1</span> <span class="bp">=</span> <span class="mi">1</span>
  <span class="n">map_mul</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">f</span> <span class="n">g</span> <span class="n">g&#39;</span><span class="o">,</span> <span class="n">toFun</span> <span class="n">f</span> <span class="o">(</span><span class="n">g</span> <span class="bp">*</span> <span class="n">g&#39;</span><span class="o">)</span> <span class="bp">=</span> <span class="n">toFun</span> <span class="n">f</span> <span class="n">g</span> <span class="bp">*</span> <span class="n">toFun</span> <span class="n">f</span> <span class="n">g&#39;</span>

<span class="kd">instance</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">N</span><span class="o">]</span> <span class="o">[</span><span class="n">MonoidHomClass&#8322;</span> <span class="n">F</span> <span class="n">M</span> <span class="n">N</span><span class="o">]</span> <span class="o">:</span> <span class="n">CoeFun</span> <span class="n">F</span> <span class="o">(</span><span class="k">fun</span> <span class="n">_</span> <span class="bp">&#8614;</span> <span class="n">M</span> <span class="bp">&#8594;</span> <span class="n">N</span><span class="o">)</span> <span class="n">where</span>
  <span class="n">coe</span> <span class="o">:=</span> <span class="n">MonoidHomClass&#8322;.toFun</span>

<span class="kn">attribute</span> <span class="o">[</span><span class="n">coe</span><span class="o">]</span> <span class="n">MonoidHomClass&#8322;.toFun</span>
</pre></div>
</div>
<p>Now we can proceed with our plan to instantiate this class.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span> <span class="o">(</span><span class="n">M</span> <span class="n">N</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">N</span><span class="o">]</span> <span class="o">:</span> <span class="n">MonoidHomClass&#8322;</span> <span class="o">(</span><span class="n">MonoidHom&#8321;</span> <span class="n">M</span> <span class="n">N</span><span class="o">)</span> <span class="n">M</span> <span class="n">N</span> <span class="n">where</span>
  <span class="n">toFun</span> <span class="o">:=</span> <span class="n">MonoidHom&#8321;.toFun</span>
  <span class="n">map_one</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">f</span> <span class="bp">&#8614;</span> <span class="n">f.map_one</span>
  <span class="n">map_mul</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">f</span> <span class="bp">&#8614;</span> <span class="n">f.map_mul</span>

<span class="kd">instance</span> <span class="o">(</span><span class="n">R</span> <span class="n">S</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">Ring</span> <span class="n">R</span><span class="o">]</span> <span class="o">[</span><span class="n">Ring</span> <span class="n">S</span><span class="o">]</span> <span class="o">:</span> <span class="n">MonoidHomClass&#8322;</span> <span class="o">(</span><span class="n">RingHom&#8321;</span> <span class="n">R</span> <span class="n">S</span><span class="o">)</span> <span class="n">R</span> <span class="n">S</span> <span class="n">where</span>
  <span class="n">toFun</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">f</span> <span class="bp">&#8614;</span> <span class="n">f.toMonoidHom&#8321;.toFun</span>
  <span class="n">map_one</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">f</span> <span class="bp">&#8614;</span> <span class="n">f.toMonoidHom&#8321;.map_one</span>
  <span class="n">map_mul</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">f</span> <span class="bp">&#8614;</span> <span class="n">f.toMonoidHom&#8321;.map_mul</span>
</pre></div>
</div>
<p>As promised every lemma we prove about <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">F</span></code> assuming an instance of <code class="docutils literal notranslate"><span class="pre">MonoidHomClass&#8321;</span> <span class="pre">F</span></code> will
apply both to monoid morphisms and ring morphisms.
Let us see an example lemma and check it applies to both situations.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">lemma</span> <span class="n">map_inv_of_inv</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">N</span><span class="o">]</span> <span class="o">[</span><span class="n">MonoidHomClass&#8322;</span> <span class="n">F</span> <span class="n">M</span> <span class="n">N</span><span class="o">]</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">F</span><span class="o">)</span> <span class="o">{</span><span class="n">m</span> <span class="n">m&#39;</span> <span class="o">:</span> <span class="n">M</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">m</span><span class="bp">*</span><span class="n">m&#39;</span> <span class="bp">=</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">f</span> <span class="n">m</span> <span class="bp">*</span> <span class="n">f</span> <span class="n">m&#39;</span> <span class="bp">=</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">rw</span> <span class="o">[</span><span class="bp">&#8592;</span> <span class="n">MonoidHomClass&#8322;.map_mul</span><span class="o">,</span> <span class="n">h</span><span class="o">,</span> <span class="n">MonoidHomClass&#8322;.map_one</span><span class="o">]</span>

<span class="kd">example</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">N</span><span class="o">]</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">MonoidHom&#8321;</span> <span class="n">M</span> <span class="n">N</span><span class="o">)</span> <span class="o">{</span><span class="n">m</span> <span class="n">m&#39;</span> <span class="o">:</span> <span class="n">M</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">m</span><span class="bp">*</span><span class="n">m&#39;</span> <span class="bp">=</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:</span> <span class="n">f</span> <span class="n">m</span> <span class="bp">*</span> <span class="n">f</span> <span class="n">m&#39;</span> <span class="bp">=</span> <span class="mi">1</span> <span class="o">:=</span>
<span class="n">map_inv_of_inv</span> <span class="n">f</span> <span class="n">h</span>

<span class="kd">example</span> <span class="o">[</span><span class="n">Ring</span> <span class="n">R</span><span class="o">]</span> <span class="o">[</span><span class="n">Ring</span> <span class="n">S</span><span class="o">]</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">RingHom&#8321;</span> <span class="n">R</span> <span class="n">S</span><span class="o">)</span> <span class="o">{</span><span class="n">r</span> <span class="n">r&#39;</span> <span class="o">:</span> <span class="n">R</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">r</span><span class="bp">*</span><span class="n">r&#39;</span> <span class="bp">=</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:</span> <span class="n">f</span> <span class="n">r</span> <span class="bp">*</span> <span class="n">f</span> <span class="n">r&#39;</span> <span class="bp">=</span> <span class="mi">1</span> <span class="o">:=</span>
<span class="n">map_inv_of_inv</span> <span class="n">f</span> <span class="n">h</span>
</pre></div>
</div>
<p>At first sight, it may look like we got back to our old bad idea of making <code class="docutils literal notranslate"><span class="pre">MonoidHom&#8321;</span></code> a class.
But we haven&#8217;t. Everything is shifted one level of abstraction up. The type class resolution
procedure won&#8217;t be looking for functions, it will be looking for either
<code class="docutils literal notranslate"><span class="pre">MonoidHom&#8321;</span></code> or <code class="docutils literal notranslate"><span class="pre">RingHom&#8321;</span></code>.</p>
<p>One remaining issue with our approach is the presence of repetitive code around the <code class="docutils literal notranslate"><span class="pre">toFun</span></code>
field and the corresponding <code class="docutils literal notranslate"><span class="pre">CoeFun</span></code> instance and <code class="docutils literal notranslate"><span class="pre">coe</span></code> attribute. It would also be better
to record that this pattern is used only for functions with extra properties, meaning that the
coercion to functions should be injective. So Mathlib adds one more layer of abstraction with
the base class <code class="docutils literal notranslate"><span class="pre">DFunLike</span></code> (where &#8220;DFun&#8221; stands for dependent function).
Let us redefine our <code class="docutils literal notranslate"><span class="pre">MonoidHomClass</span></code> on top of this base layer.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">MonoidHomClass&#8323;</span> <span class="o">(</span><span class="n">F</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">(</span><span class="n">M</span> <span class="n">N</span> <span class="o">:</span> <span class="n">outParam</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">N</span><span class="o">]</span> <span class="kd">extends</span>
    <span class="n">DFunLike</span> <span class="n">F</span> <span class="n">M</span> <span class="o">(</span><span class="k">fun</span> <span class="n">_</span> <span class="bp">&#8614;</span> <span class="n">N</span><span class="o">)</span> <span class="n">where</span>
  <span class="n">map_one</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">f</span> <span class="o">:</span> <span class="n">F</span><span class="o">,</span> <span class="n">f</span> <span class="mi">1</span> <span class="bp">=</span> <span class="mi">1</span>
  <span class="n">map_mul</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">F</span><span class="o">)</span> <span class="n">g</span> <span class="n">g&#39;</span><span class="o">,</span> <span class="n">f</span> <span class="o">(</span><span class="n">g</span> <span class="bp">*</span> <span class="n">g&#39;</span><span class="o">)</span> <span class="bp">=</span> <span class="n">f</span> <span class="n">g</span> <span class="bp">*</span> <span class="n">f</span> <span class="n">g&#39;</span>

<span class="kd">instance</span> <span class="o">(</span><span class="n">M</span> <span class="n">N</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">N</span><span class="o">]</span> <span class="o">:</span> <span class="n">MonoidHomClass&#8323;</span> <span class="o">(</span><span class="n">MonoidHom&#8321;</span> <span class="n">M</span> <span class="n">N</span><span class="o">)</span> <span class="n">M</span> <span class="n">N</span> <span class="n">where</span>
  <span class="n">coe</span> <span class="o">:=</span> <span class="n">MonoidHom&#8321;.toFun</span>
  <span class="n">coe_injective&#39;</span> <span class="o">:=</span> <span class="n">MonoidHom&#8321;.ext</span>
  <span class="n">map_one</span> <span class="o">:=</span> <span class="n">MonoidHom&#8321;.map_one</span>
  <span class="n">map_mul</span> <span class="o">:=</span> <span class="n">MonoidHom&#8321;.map_mul</span>
</pre></div>
</div>
<p>Of course the hierarchy of morphisms does not stop here. We could go on and define a class
<code class="docutils literal notranslate"><span class="pre">RingHomClass&#8323;</span></code> extending <code class="docutils literal notranslate"><span class="pre">MonoidHomClass&#8323;</span></code> and instantiate it on <code class="docutils literal notranslate"><span class="pre">RingHom</span></code> and
then later on <code class="docutils literal notranslate"><span class="pre">AlgebraHom</span></code> (algebras are rings with some extra structure). But we&#8217;ve
covered the main formalization ideas used in Mathlib for morphisms and you should be ready
to understand how morphisms are defined in Mathlib.</p>
<p>As an exercise, you should try to define your class of bundled order-preserving function between
ordered types, and then order preserving monoid morphisms. This is for training purposes only.
Like continuous functions, order preserving functions are primarily unbundled in Mathlib where
they are defined by the <code class="docutils literal notranslate"><span class="pre">Monotone</span></code> predicate. Of course you need to complete the class
definitions below.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[ext]</span>
<span class="kd">structure</span> <span class="n">OrderPresHom</span> <span class="o">(</span><span class="n">&#945;</span> <span class="n">&#946;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">LE</span> <span class="n">&#945;</span><span class="o">]</span> <span class="o">[</span><span class="n">LE</span> <span class="n">&#946;</span><span class="o">]</span> <span class="n">where</span>
  <span class="n">toFun</span> <span class="o">:</span> <span class="n">&#945;</span> <span class="bp">&#8594;</span> <span class="n">&#946;</span>
  <span class="n">le_of_le</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">a</span> <span class="n">a&#39;</span><span class="o">,</span> <span class="n">a</span> <span class="bp">&#8804;</span> <span class="n">a&#39;</span> <span class="bp">&#8594;</span> <span class="n">toFun</span> <span class="n">a</span> <span class="bp">&#8804;</span> <span class="n">toFun</span> <span class="n">a&#39;</span>

<span class="kd">@[ext]</span>
<span class="kd">structure</span> <span class="n">OrderPresMonoidHom</span> <span class="o">(</span><span class="n">M</span> <span class="n">N</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">[</span><span class="n">LE</span> <span class="n">M</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">N</span><span class="o">]</span> <span class="o">[</span><span class="n">LE</span> <span class="n">N</span><span class="o">]</span> <span class="kd">extends</span>
<span class="n">MonoidHom&#8321;</span> <span class="n">M</span> <span class="n">N</span><span class="o">,</span> <span class="n">OrderPresHom</span> <span class="n">M</span> <span class="n">N</span>

<span class="kd">class</span> <span class="n">OrderPresHomClass</span> <span class="o">(</span><span class="n">F</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">(</span><span class="n">&#945;</span> <span class="n">&#946;</span> <span class="o">:</span> <span class="n">outParam</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">LE</span> <span class="n">&#945;</span><span class="o">]</span> <span class="o">[</span><span class="n">LE</span> <span class="n">&#946;</span><span class="o">]</span>

<span class="kd">instance</span> <span class="o">(</span><span class="n">&#945;</span> <span class="n">&#946;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">LE</span> <span class="n">&#945;</span><span class="o">]</span> <span class="o">[</span><span class="n">LE</span> <span class="n">&#946;</span><span class="o">]</span> <span class="o">:</span> <span class="n">OrderPresHomClass</span> <span class="o">(</span><span class="n">OrderPresHom</span> <span class="n">&#945;</span> <span class="n">&#946;</span><span class="o">)</span> <span class="n">&#945;</span> <span class="n">&#946;</span> <span class="n">where</span>

<span class="kd">instance</span> <span class="o">(</span><span class="n">&#945;</span> <span class="n">&#946;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">LE</span> <span class="n">&#945;</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">&#945;</span><span class="o">]</span> <span class="o">[</span><span class="n">LE</span> <span class="n">&#946;</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">&#946;</span><span class="o">]</span> <span class="o">:</span>
    <span class="n">OrderPresHomClass</span> <span class="o">(</span><span class="n">OrderPresMonoidHom</span> <span class="n">&#945;</span> <span class="n">&#946;</span><span class="o">)</span> <span class="n">&#945;</span> <span class="n">&#946;</span> <span class="n">where</span>

<span class="kd">instance</span> <span class="o">(</span><span class="n">&#945;</span> <span class="n">&#946;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">LE</span> <span class="n">&#945;</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">&#945;</span><span class="o">]</span> <span class="o">[</span><span class="n">LE</span> <span class="n">&#946;</span><span class="o">]</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">&#946;</span><span class="o">]</span> <span class="o">:</span>
    <span class="n">MonoidHomClass&#8323;</span> <span class="o">(</span><span class="n">OrderPresMonoidHom</span> <span class="n">&#945;</span> <span class="n">&#946;</span><span class="o">)</span> <span class="n">&#945;</span> <span class="n">&#946;</span>
  <span class="o">:=</span> <span class="gr">sorry</span>
</pre></div>
</div>
</div>
<div class="section" id="sub-objects">
<span id="section-hierarchies-subobjects"></span><h2><span class="section-number">7.3. </span>Sub-objects<a class="headerlink" href="#sub-objects" title="Permalink to this headline">&#61633;</a></h2>
<p>After defining some algebraic structure and its morphisms, the next step is to consider sets
that inherit this algebraic structure, for instance subgroups or subrings.
This largely overlaps with our previous topic. Indeed a set in <code class="docutils literal notranslate"><span class="pre">X</span></code> is implemented as a function from
<code class="docutils literal notranslate"><span class="pre">X</span></code> to <code class="docutils literal notranslate"><span class="pre">Prop</span></code> so sub-objects are function satisfying a certain predicate.
Hence we can reuse of lot of the ideas that led to the <code class="docutils literal notranslate"><span class="pre">DFunLike</span></code> class and its descendants.
We won&#8217;t reuse <code class="docutils literal notranslate"><span class="pre">DFunLike</span></code> itself because this would break the abstraction barrier from <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">X</span></code>
to <code class="docutils literal notranslate"><span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">Prop</span></code>. Instead there is a <code class="docutils literal notranslate"><span class="pre">SetLike</span></code> class. Instead of wrapping an injection into a
function type, that class wraps an injection into a <code class="docutils literal notranslate"><span class="pre">Set</span></code> type and defines the corresponding
coercion and <code class="docutils literal notranslate"><span class="pre">Membership</span></code> instance.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[ext]</span>
<span class="kd">structure</span> <span class="n">Submonoid&#8321;</span> <span class="o">(</span><span class="n">M</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="n">where</span>
  <span class="sd">/-- The carrier of a submonoid. -/</span>
  <span class="n">carrier</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">M</span>
  <span class="sd">/-- The product of two elements of a submonoid belongs to the submonoid. -/</span>
  <span class="n">mul_mem</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span><span class="o">}</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8712;</span> <span class="n">carrier</span> <span class="bp">&#8594;</span> <span class="n">b</span> <span class="bp">&#8712;</span> <span class="n">carrier</span> <span class="bp">&#8594;</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">&#8712;</span> <span class="n">carrier</span>
  <span class="sd">/-- The unit element belongs to the submonoid. -/</span>
  <span class="n">one_mem</span> <span class="o">:</span> <span class="mi">1</span> <span class="bp">&#8712;</span> <span class="n">carrier</span>

<span class="sd">/-- Submonoids in `M` can be seen as sets in `M`. -/</span>
<span class="kd">instance</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">:</span> <span class="n">SetLike</span> <span class="o">(</span><span class="n">Submonoid&#8321;</span> <span class="n">M</span><span class="o">)</span> <span class="n">M</span> <span class="n">where</span>
  <span class="n">coe</span> <span class="o">:=</span> <span class="n">Submonoid&#8321;.carrier</span>
  <span class="n">coe_injective&#39;</span> <span class="o">:=</span> <span class="n">Submonoid&#8321;.ext</span>
</pre></div>
</div>
<p>Equipped with the above <code class="docutils literal notranslate"><span class="pre">SetLike</span></code> instance, we can already state naturally that
a submonoid <code class="docutils literal notranslate"><span class="pre">N</span></code> contains <code class="docutils literal notranslate"><span class="pre">1</span></code> without using <code class="docutils literal notranslate"><span class="pre">N.carrier</span></code>.
We can also silently treat <code class="docutils literal notranslate"><span class="pre">N</span></code> as a set in <code class="docutils literal notranslate"><span class="pre">M</span></code> as take its direct image under a map.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">(</span><span class="n">N</span> <span class="o">:</span> <span class="n">Submonoid&#8321;</span> <span class="n">M</span><span class="o">)</span> <span class="o">:</span> <span class="mi">1</span> <span class="bp">&#8712;</span> <span class="n">N</span> <span class="o">:=</span> <span class="n">N.one_mem</span>

<span class="kd">example</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">(</span><span class="n">N</span> <span class="o">:</span> <span class="n">Submonoid&#8321;</span> <span class="n">M</span><span class="o">)</span> <span class="o">(</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">M</span> <span class="bp">&#8594;</span> <span class="n">&#945;</span><span class="o">)</span> <span class="o">:=</span> <span class="n">f</span> <span class="bp">&#39;&#39;</span> <span class="n">N</span>
</pre></div>
</div>
<p>We also have a coercion to <code class="docutils literal notranslate"><span class="pre">Type</span></code> which uses <code class="docutils literal notranslate"><span class="pre">Subtype</span></code> so, given a submonoid <code class="docutils literal notranslate"><span class="pre">N</span></code> we can write
a parameter <code class="docutils literal notranslate"><span class="pre">(x</span> <span class="pre">:</span> <span class="pre">N)</span></code> which can be coerced to an element of <code class="docutils literal notranslate"><span class="pre">M</span></code> belonging to <code class="docutils literal notranslate"><span class="pre">N</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">(</span><span class="n">N</span> <span class="o">:</span> <span class="n">Submonoid&#8321;</span> <span class="n">M</span><span class="o">)</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">N</span><span class="o">)</span> <span class="o">:</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">M</span><span class="o">)</span> <span class="bp">&#8712;</span> <span class="n">N</span> <span class="o">:=</span> <span class="n">x.property</span>
</pre></div>
</div>
<p>Using this coercion to <code class="docutils literal notranslate"><span class="pre">Type</span></code> we can also tackle the task of equipping a submonoid with a
monoid structure. We will use the coercion from the type associated to <code class="docutils literal notranslate"><span class="pre">N</span></code> as above, and the
lemma <code class="docutils literal notranslate"><span class="pre">SetCoe.ext</span></code> asserting this coercion is injective. Both are provided by the <code class="docutils literal notranslate"><span class="pre">SetLike</span></code>
instance.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span> <span class="n">SubMonoid&#8321;Monoid</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">(</span><span class="n">N</span> <span class="o">:</span> <span class="n">Submonoid&#8321;</span> <span class="n">M</span><span class="o">)</span> <span class="o">:</span> <span class="n">Monoid</span> <span class="n">N</span> <span class="n">where</span>
  <span class="n">mul</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">x</span> <span class="n">y</span> <span class="bp">&#8614;</span> <span class="o">&#10216;</span><span class="n">x</span><span class="bp">*</span><span class="n">y</span><span class="o">,</span> <span class="n">N.mul_mem</span> <span class="n">x.property</span> <span class="n">y.property</span><span class="o">&#10217;</span>
  <span class="n">mul_assoc</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">x</span> <span class="n">y</span> <span class="n">z</span> <span class="bp">&#8614;</span> <span class="n">SetCoe.ext</span> <span class="o">(</span><span class="n">mul_assoc</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">M</span><span class="o">)</span> <span class="n">y</span> <span class="n">z</span><span class="o">)</span>
  <span class="n">one</span> <span class="o">:=</span> <span class="o">&#10216;</span><span class="mi">1</span><span class="o">,</span> <span class="n">N.one_mem</span><span class="o">&#10217;</span>
  <span class="n">one_mul</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">x</span> <span class="bp">&#8614;</span> <span class="n">SetCoe.ext</span> <span class="o">(</span><span class="n">one_mul</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">M</span><span class="o">))</span>
  <span class="n">mul_one</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">x</span> <span class="bp">&#8614;</span> <span class="n">SetCoe.ext</span> <span class="o">(</span><span class="n">mul_one</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">M</span><span class="o">))</span>
</pre></div>
</div>
<p>Note that, in the above instance, instead of using the coercion to <code class="docutils literal notranslate"><span class="pre">M</span></code> and calling the
<code class="docutils literal notranslate"><span class="pre">property</span></code> field, we could have used destructuring binders as follows.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">(</span><span class="n">N</span> <span class="o">:</span> <span class="n">Submonoid&#8321;</span> <span class="n">M</span><span class="o">)</span> <span class="o">:</span> <span class="n">Monoid</span> <span class="n">N</span> <span class="n">where</span>
  <span class="n">mul</span> <span class="o">:=</span> <span class="k">fun</span> <span class="o">&#10216;</span><span class="n">x</span><span class="o">,</span> <span class="n">hx</span><span class="o">&#10217;</span> <span class="o">&#10216;</span><span class="n">y</span><span class="o">,</span> <span class="n">hy</span><span class="o">&#10217;</span> <span class="bp">&#8614;</span> <span class="o">&#10216;</span><span class="n">x</span><span class="bp">*</span><span class="n">y</span><span class="o">,</span> <span class="n">N.mul_mem</span> <span class="n">hx</span> <span class="n">hy</span><span class="o">&#10217;</span>
  <span class="n">mul_assoc</span> <span class="o">:=</span> <span class="k">fun</span> <span class="o">&#10216;</span><span class="n">x</span><span class="o">,</span> <span class="n">_</span><span class="o">&#10217;</span> <span class="o">&#10216;</span><span class="n">y</span><span class="o">,</span> <span class="n">_</span><span class="o">&#10217;</span> <span class="o">&#10216;</span><span class="n">z</span><span class="o">,</span> <span class="n">_</span><span class="o">&#10217;</span> <span class="bp">&#8614;</span> <span class="n">SetCoe.ext</span> <span class="o">(</span><span class="n">mul_assoc</span> <span class="n">x</span> <span class="n">y</span> <span class="n">z</span><span class="o">)</span>
  <span class="n">one</span> <span class="o">:=</span> <span class="o">&#10216;</span><span class="mi">1</span><span class="o">,</span> <span class="n">N.one_mem</span><span class="o">&#10217;</span>
  <span class="n">one_mul</span> <span class="o">:=</span> <span class="k">fun</span> <span class="o">&#10216;</span><span class="n">x</span><span class="o">,</span> <span class="n">_</span><span class="o">&#10217;</span> <span class="bp">&#8614;</span> <span class="n">SetCoe.ext</span> <span class="o">(</span><span class="n">one_mul</span> <span class="n">x</span><span class="o">)</span>
  <span class="n">mul_one</span> <span class="o">:=</span> <span class="k">fun</span> <span class="o">&#10216;</span><span class="n">x</span><span class="o">,</span> <span class="n">_</span><span class="o">&#10217;</span> <span class="bp">&#8614;</span> <span class="n">SetCoe.ext</span> <span class="o">(</span><span class="n">mul_one</span> <span class="n">x</span><span class="o">)</span>
</pre></div>
</div>
<p>In order to apply lemmas about submonoids to subgroups or subrings, we need a class, just
like for morphisms. Note this class take a <code class="docutils literal notranslate"><span class="pre">SetLike</span></code> instance as a parameter so it does not need
a carrier field and can use the membership notation in its fields.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">class</span> <span class="n">SubmonoidClass&#8321;</span> <span class="o">(</span><span class="n">S</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">(</span><span class="n">M</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">[</span><span class="n">SetLike</span> <span class="n">S</span> <span class="n">M</span><span class="o">]</span> <span class="o">:</span> <span class="kt">Prop</span> <span class="n">where</span>
  <span class="n">mul_mem</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">s</span> <span class="o">:</span> <span class="n">S</span><span class="o">)</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">M</span><span class="o">},</span> <span class="n">a</span> <span class="bp">&#8712;</span> <span class="n">s</span> <span class="bp">&#8594;</span> <span class="n">b</span> <span class="bp">&#8712;</span> <span class="n">s</span> <span class="bp">&#8594;</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">&#8712;</span> <span class="n">s</span>
  <span class="n">one_mem</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">s</span> <span class="o">:</span> <span class="n">S</span><span class="o">,</span> <span class="mi">1</span> <span class="bp">&#8712;</span> <span class="n">s</span>

<span class="kd">instance</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">:</span> <span class="n">SubmonoidClass&#8321;</span> <span class="o">(</span><span class="n">Submonoid&#8321;</span> <span class="n">M</span><span class="o">)</span> <span class="n">M</span> <span class="n">where</span>
  <span class="n">mul_mem</span> <span class="o">:=</span> <span class="n">Submonoid&#8321;.mul_mem</span>
  <span class="n">one_mem</span> <span class="o">:=</span> <span class="n">Submonoid&#8321;.one_mem</span>
</pre></div>
</div>
<p>As an exercise you should define a <code class="docutils literal notranslate"><span class="pre">Subgroup&#8321;</span></code> structure, endow it with a <code class="docutils literal notranslate"><span class="pre">SetLike</span></code> instance
and a <code class="docutils literal notranslate"><span class="pre">SubmonoidClass&#8321;</span></code> instance, put a <code class="docutils literal notranslate"><span class="pre">Group</span></code> instance on the subtype associated to a
<code class="docutils literal notranslate"><span class="pre">Subgroup&#8321;</span></code> and define a <code class="docutils literal notranslate"><span class="pre">SubgroupClass&#8321;</span></code> class.</p>
<p>Another very important thing to know about subobjects of a given algebraic object in Mathlib
always form a complete lattice, and this structure is used a lot. For instance you may look for
the lemma saying that an intersection of submonoids is a submonoid. But this won&#8217;t be a lemma,
this will be an infimum construction. Let us do the case of two submonoids.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">instance</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">:</span> <span class="n">Inf</span> <span class="o">(</span><span class="n">Submonoid&#8321;</span> <span class="n">M</span><span class="o">)</span> <span class="o">:=</span>
  <span class="o">&#10216;</span><span class="k">fun</span> <span class="n">S&#8321;</span> <span class="n">S&#8322;</span> <span class="bp">&#8614;</span>
    <span class="o">{</span> <span class="n">carrier</span> <span class="o">:=</span> <span class="n">S&#8321;</span> <span class="bp">&#8745;</span> <span class="n">S&#8322;</span>
      <span class="n">one_mem</span> <span class="o">:=</span> <span class="o">&#10216;</span><span class="n">S&#8321;.one_mem</span><span class="o">,</span> <span class="n">S&#8322;.one_mem</span><span class="o">&#10217;</span>
      <span class="n">mul_mem</span> <span class="o">:=</span> <span class="k">fun</span> <span class="o">&#10216;</span><span class="n">hx</span><span class="o">,</span> <span class="n">hx&#39;</span><span class="o">&#10217;</span> <span class="o">&#10216;</span><span class="n">hy</span><span class="o">,</span> <span class="n">hy&#39;</span><span class="o">&#10217;</span> <span class="bp">&#8614;</span> <span class="o">&#10216;</span><span class="n">S&#8321;.mul_mem</span> <span class="n">hx</span> <span class="n">hy</span><span class="o">,</span> <span class="n">S&#8322;.mul_mem</span> <span class="n">hx&#39;</span> <span class="n">hy&#39;</span><span class="o">&#10217;</span> <span class="o">}&#10217;</span>
</pre></div>
</div>
<p>This allows to get the intersections of two submonoids as a submonoid.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">[</span><span class="n">Monoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">(</span><span class="n">N</span> <span class="n">P</span> <span class="o">:</span> <span class="n">Submonoid&#8321;</span> <span class="n">M</span><span class="o">)</span> <span class="o">:</span> <span class="n">Submonoid&#8321;</span> <span class="n">M</span> <span class="o">:=</span> <span class="n">N</span> <span class="bp">&#8851;</span> <span class="n">P</span>
</pre></div>
</div>
<p>You may think it&#8217;s a shame that we had to use the inf symbol <code class="docutils literal notranslate"><span class="pre">&#8851;</span></code> in the above example instead
of the intersection symbol <code class="docutils literal notranslate"><span class="pre">&#8745;</span></code>. But think about the supremum. The union of two submonoids is not
a submonoid. However submonoids still form a lattice (even a complete one). Actually <code class="docutils literal notranslate"><span class="pre">N</span> <span class="pre">&#8852;</span> <span class="pre">P</span></code> is
the submonoid generated by the union of <code class="docutils literal notranslate"><span class="pre">N</span></code> and <code class="docutils literal notranslate"><span class="pre">P</span></code> and of course it would be very confusing to
denote it by <code class="docutils literal notranslate"><span class="pre">N</span> <span class="pre">&#8746;</span> <span class="pre">P</span></code>. So you can see the use of <code class="docutils literal notranslate"><span class="pre">N</span> <span class="pre">&#8851;</span> <span class="pre">P</span></code> as much more consistent. It is also
a lot more consistent across various kind of algebraic structures. It may look a bit weird at first
to see the sum of two vector subspace <code class="docutils literal notranslate"><span class="pre">E</span></code> and <code class="docutils literal notranslate"><span class="pre">F</span></code> denoted by <code class="docutils literal notranslate"><span class="pre">E</span> <span class="pre">&#8852;</span> <span class="pre">F</span></code> instead of <code class="docutils literal notranslate"><span class="pre">E</span> <span class="pre">+</span> <span class="pre">F</span></code>.
But you will get used to it. And soon you will consider the <code class="docutils literal notranslate"><span class="pre">E</span> <span class="pre">+</span> <span class="pre">F</span></code> notation as a distraction
emphasizing the anecdotal fact that elements of <code class="docutils literal notranslate"><span class="pre">E</span> <span class="pre">&#8852;</span> <span class="pre">F</span></code> can be written as a sum of an element of
<code class="docutils literal notranslate"><span class="pre">E</span></code> and an element of <code class="docutils literal notranslate"><span class="pre">F</span></code> instead of emphasizing the fundamental fact that <code class="docutils literal notranslate"><span class="pre">E</span> <span class="pre">&#8852;</span> <span class="pre">F</span></code> is the
smallest vector subspace containing both <code class="docutils literal notranslate"><span class="pre">E</span></code> and <code class="docutils literal notranslate"><span class="pre">F</span></code>.</p>
<p>Our last topic for this chapter is that of quotients. Again we want to explain how
convenient notation are built and code duplication is avoided in Mathlib. Here the main device
is the <code class="docutils literal notranslate"><span class="pre">HasQuotient</span></code> class which allows notations like <code class="docutils literal notranslate"><span class="pre">M</span> <span class="pre">&#10744;</span> <span class="pre">N</span></code>. Beware the quotient symbol
<code class="docutils literal notranslate"><span class="pre">&#10744;</span></code> is a special unicode character, not a regular ASCII division symbol.</p>
<p>As an example, we will build the quotient of a commutative monoid by a submonoid, leave proofs
to you. In the last example, you can use <code class="docutils literal notranslate"><span class="pre">Setoid.refl</span></code> but it won&#8217;t automatically pick up
the relevant <code class="docutils literal notranslate"><span class="pre">Setoid</span></code> structure. You can fix this issue by providing all arguments using
the <code class="docutils literal notranslate"><span class="pre">&#64;</span></code> syntax, as in <code class="docutils literal notranslate"><span class="pre">&#64;Setoid.refl</span> <span class="pre">M</span> <span class="pre">N.Setoid</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">Submonoid.Setoid</span> <span class="o">[</span><span class="n">CommMonoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">(</span><span class="n">N</span> <span class="o">:</span> <span class="n">Submonoid</span> <span class="n">M</span><span class="o">)</span> <span class="o">:</span> <span class="n">Setoid</span> <span class="n">M</span>  <span class="n">where</span>
  <span class="n">r</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">x</span> <span class="n">y</span> <span class="bp">&#8614;</span> <span class="bp">&#8707;</span> <span class="n">w</span> <span class="bp">&#8712;</span> <span class="n">N</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">z</span> <span class="bp">&#8712;</span> <span class="n">N</span><span class="o">,</span> <span class="n">x</span><span class="bp">*</span><span class="n">w</span> <span class="bp">=</span> <span class="n">y</span><span class="bp">*</span><span class="n">z</span>
  <span class="n">iseqv</span> <span class="o">:=</span> <span class="o">{</span>
    <span class="n">refl</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">x</span> <span class="bp">&#8614;</span> <span class="o">&#10216;</span><span class="mi">1</span><span class="o">,</span> <span class="n">N.one_mem</span><span class="o">,</span> <span class="mi">1</span><span class="o">,</span> <span class="n">N.one_mem</span><span class="o">,</span> <span class="n">rfl</span><span class="o">&#10217;</span>
    <span class="n">symm</span> <span class="o">:=</span> <span class="k">fun</span> <span class="o">&#10216;</span><span class="n">w</span><span class="o">,</span> <span class="n">hw</span><span class="o">,</span> <span class="n">z</span><span class="o">,</span> <span class="n">hz</span><span class="o">,</span> <span class="n">h</span><span class="o">&#10217;</span> <span class="bp">&#8614;</span> <span class="o">&#10216;</span><span class="n">z</span><span class="o">,</span> <span class="n">hz</span><span class="o">,</span> <span class="n">w</span><span class="o">,</span> <span class="n">hw</span><span class="o">,</span> <span class="n">h.symm</span><span class="o">&#10217;</span>
    <span class="n">trans</span> <span class="o">:=</span> <span class="kd">by</span>
      <span class="gr">sorry</span>
  <span class="o">}</span>

<span class="kd">instance</span> <span class="o">[</span><span class="n">CommMonoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">:</span> <span class="n">HasQuotient</span> <span class="n">M</span> <span class="o">(</span><span class="n">Submonoid</span> <span class="n">M</span><span class="o">)</span> <span class="n">where</span>
  <span class="n">quotient&#39;</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">N</span> <span class="bp">&#8614;</span> <span class="n">Quotient</span> <span class="n">N.Setoid</span>

<span class="kd">def</span> <span class="n">QuotientMonoid.mk</span> <span class="o">[</span><span class="n">CommMonoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">(</span><span class="n">N</span> <span class="o">:</span> <span class="n">Submonoid</span> <span class="n">M</span><span class="o">)</span> <span class="o">:</span> <span class="n">M</span> <span class="bp">&#8594;</span> <span class="n">M</span> <span class="bp">&#10744;</span> <span class="n">N</span> <span class="o">:=</span> <span class="n">Quotient.mk</span> <span class="n">N.Setoid</span>

<span class="kd">instance</span> <span class="o">[</span><span class="n">CommMonoid</span> <span class="n">M</span><span class="o">]</span> <span class="o">(</span><span class="n">N</span> <span class="o">:</span> <span class="n">Submonoid</span> <span class="n">M</span><span class="o">)</span> <span class="o">:</span> <span class="n">Monoid</span> <span class="o">(</span><span class="n">M</span> <span class="bp">&#10744;</span> <span class="n">N</span><span class="o">)</span> <span class="n">where</span>
  <span class="n">mul</span> <span class="o">:=</span> <span class="n">Quotient.map&#8322;&#39;</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">*</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">(</span><span class="kd">by</span>
      <span class="gr">sorry</span>
        <span class="o">)</span>
  <span class="n">mul_assoc</span> <span class="o">:=</span> <span class="kd">by</span>
      <span class="gr">sorry</span>
  <span class="n">one</span> <span class="o">:=</span> <span class="n">QuotientMonoid.mk</span> <span class="n">N</span> <span class="mi">1</span>
  <span class="n">one_mul</span> <span class="o">:=</span> <span class="kd">by</span>
      <span class="gr">sorry</span>
  <span class="n">mul_one</span> <span class="o">:=</span> <span class="kd">by</span>
      <span class="gr">sorry</span>
</pre></div>
</div>
</div>
</div>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="C06_Structures.html" class="btn btn-neutral float-left" title="6. Structures" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="C08_Groups_and_Rings.html" class="btn btn-neutral float-right" title="8. Groups and Rings" 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, Jeremy Avigad, Patrick Massot.</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>