Commit 3b1b8e3
committed
made UniversalMorphismIntoDirectProductWithGivenDirectProduct purely functional
for SkeletalFinSets1 parent 8a30559 commit 3b1b8e3
File tree
4 files changed
+40
-23
lines changed- examples
- gap
- precompiled_categories
4 files changed
+40
-23
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
10 | 10 | | |
11 | 11 | | |
12 | 12 | | |
13 | | - | |
| 13 | + | |
14 | 14 | | |
15 | 15 | | |
16 | 16 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
12 | 12 | | |
13 | 13 | | |
14 | 14 | | |
15 | | - | |
16 | | - | |
17 | | - | |
18 | 15 | | |
19 | 16 | | |
20 | 17 | | |
21 | 18 | | |
22 | 19 | | |
23 | | - | |
24 | | - | |
25 | | - | |
26 | | - | |
27 | | - | |
28 | | - | |
29 | | - | |
30 | | - | |
| 20 | + | |
31 | 21 | | |
32 | 22 | | |
33 | 23 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
543 | 543 | | |
544 | 544 | | |
545 | 545 | | |
546 | | - | |
547 | | - | |
| 546 | + | |
| 547 | + | |
| 548 | + | |
548 | 549 | | |
549 | | - | |
550 | | - | |
| 550 | + | |
551 | 551 | | |
552 | | - | |
| 552 | + | |
553 | 553 | | |
554 | | - | |
| 554 | + | |
555 | 555 | | |
556 | | - | |
557 | | - | |
558 | | - | |
| 556 | + | |
559 | 557 | | |
560 | | - | |
| 558 | + | |
561 | 559 | | |
562 | | - | |
| 560 | + | |
563 | 561 | | |
564 | 562 | | |
565 | 563 | | |
| |||
Lines changed: 29 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
746 | 746 | | |
747 | 747 | | |
748 | 748 | | |
| 749 | + | |
| 750 | + | |
| 751 | + | |
| 752 | + | |
| 753 | + | |
| 754 | + | |
| 755 | + | |
| 756 | + | |
| 757 | + | |
| 758 | + | |
| 759 | + | |
| 760 | + | |
| 761 | + | |
| 762 | + | |
| 763 | + | |
| 764 | + | |
| 765 | + | |
| 766 | + | |
| 767 | + | |
| 768 | + | |
| 769 | + | |
| 770 | + | |
| 771 | + | |
| 772 | + | |
| 773 | + | |
| 774 | + | |
| 775 | + | |
| 776 | + | |
| 777 | + | |
749 | 778 | | |
750 | 779 | | |
751 | 780 | | |
| |||
0 commit comments