forked from metamath/set.mm
-
Notifications
You must be signed in to change notification settings - Fork 0
/
changes-set.txt
12532 lines (12526 loc) · 595 KB
/
changes-set.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
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
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Recent label changes
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
This is part of an ongoing project to improve naming consistency. If you have
suggestions for better names, let us know. It lists changes in set.mm (for
iset.mm, see the git history, although many of the proposed or historical
changes described here also apply to iset.mm, or should be adopted in iset.mm
when someone gets the chance).
To update your mathbox, you can make global substitutions into
your local version by processing the ones WITHOUT "Notes" in REVERSE order.
The ones WITH "Notes" may have to be processed manually.
PROPOSED:
Date Old New Notes
proposed syl imtri (analogous to *bitr*, sstri, etc.)
proposed sylib imbitri etc.
proposed sylbid biimtrd etc.
proposed sylbird biimtrrd etc.
proposed syl5* *trid (syl5bi -> biimtrid; syl5eqel -> eqeltrid;etc.)
proposed syl6* *trdi
proposed *mpt* *mpf* or *mptf* (maps-to for functions)
proposed *mpt2* *mpo* or *mpto* (maps-to for operations)
(Please send any comments on these proposals to the mailing list or
make a github issue.)
DONE:
Date Old New Notes
16-Apr-23 xrhaus [same] moved from TA's mathbox to main set.mm
7-Apr-23 rexsngf [same] moved from GS's mathbox to main set.mm
2-Apr-23 reuxfr4d [same] moved from TA's mathbox to main set.mm
2-Apr-23 reuxfr3d [same] moved from TA's mathbox to main set.mm
2-Apr-23 2reuswap2 [same] moved from TA's mathbox to main set.mm
2-Apr-23 pm5.31r [same] moved from RM's mathbox to main set.mm
19-Mar-23 soasym [same] moved from SF's mathbox to main set.mm
19-Mar-23 fvmptd2 [same] moved from GS's mathbox to main set.mm
15-Mar-23 mapfvd [same] moved from AV's mathbox to main set.mm
2-Mar-23 wl-hbnaev hbnaev moved from WL's mathbox to main set.mm
21-Feb-23 moimd moimdv align with mobidv, eubidv
16-Feb-23 bj-ldiv ldiv moved from BJ's mathbox to main set.mm
16-Feb-23 bj-rdiv rdiv moved from BJ's mathbox to main set.mm
16-Feb-23 bj-mdiv mdiv moved from BJ's mathbox to main set.mm
16-Feb-23 bj-lineq lineq moved from BJ's mathbox to main set.mm
16-Feb-23 subdivcomb2 [same] moved from SF's mathbox to main set.mm
16-Feb-23 negelrpd [same] moved from GS's mathbox to main set.mm
16-Feb-23 1xr [same] moved from GS's mathbox to main set.mm
16-Feb-23 rexlimdva2 [same] moved from GS's mathbox to main set.mm
16-Feb-23 mvrladdd [same] moved from DAW's mathbox to main set.mm
12-Feb-23 df-tau moved from JK's mathbox to main set.mm
10-Feb-23 rrxmetfi [same] moved from GS's mathbox to main set.mm
10-Feb-23 rrxdsfi [same] moved from GS's mathbox to main set.mm
10-Feb-23 rrxbasefi [same] moved from GS's mathbox to main set.mm
10-Feb-23 addgtge0d [same] moved from AI's mathbox to main set.mm
10-Feb-23 addeq0 [same] moved from TA's mathbox to main set.mm
10-Feb-23 assraddsubd [same] moved from DAW's mathbox to main set.mm
10-Feb-23 xpexd [same] moved from GS's mathbox to main set.mm
10-Feb-23 fvmptd3 [same] moved from GS's mathbox to main set.mm
10-Feb-23 eqeqan1d [same] moved from PM's mathbox to main set.mm
5-Feb-23 srngfn srngstr
30-Jan-23 elsb4lem elsb4v
30-Jan-23 elsb3lem elsb3v
30-Jan-23 equsb3lem equsb3v equsb3lem was a duplicate of equsb3v
19-Jan-23 bj-stdpc4v stdpc4v moved from BJ's mathbox to main set.mm
19-Jan-23 bj-sbftv sbftv moved from BJ's mathbox to main set.mm
19-Jan-23 bj-sbfv sbfv moved from BJ's mathbox to main set.mm
19-Jan-23 bj-equsb1v equsb1v moved from BJ's mathbox to main set.mm
7-Dec-22 decmul1 [same] revised - remove unneeded hypothesis
5-Dec-22 f1oeq2d [same] moved from GS's mathbox to main set.mm
5-Dec-22 dmexd [same] moved from GS's mathbox to main set.mm
13-Oct-22 rmo4f [same] moved from TA's mathbox to main set.mm
13-Oct-22 rmo3f [same] moved from TA's mathbox to main set.mm
13-Oct-22 iunxsngf [same] moved from TA's mathbox to main set.mm
12-Oct-22 df-pfx [same] definition and related theorems
moved from AV's mathbox to main set.mm
9-Oct-22 ndisj [same] moved from RP's mathbox to main set.mm
9-Oct-22 19.9alt 19.3t moved from NM's mathbox to main set.mm
7-Oct-22 exmoeu2 exmoeub biconditional form of exmoeu
7-Oct-22 eubi [same] moved from ATS's mathbox to main set.mm
6-Oct-22 hhsshl csschl hhsshl was in deprecated Part 19
6-Oct-22 hhssbn cssbn hhssbn was in deprecated Part 19
6-Oct-22 ssphl cphssphl ssphl was in deprecated Part 19
6-Oct-22 sspph cphsscph sspph was in deprecated Part 19
4-Oct-22 brresi brresi2
4-Oct-22 opelresi opelidres
4-Oct-22 brres brresi
4-Oct-22 opelres opelresi
4-Oct-22 brresALTV brres moved from PM's mathbox to main set.mm
4-Oct-22 opelresALTV opelres moved from PM's mathbox to main set.mm
4-Oct-22 inxpssres [same] moved from PM's mathbox to main set.mm
4-Oct-22 anbi1cd [same] moved from PM's mathbox to main set.mm
4-Oct-22 anbi1ci [same] moved from PM's mathbox to main set.mm
4-Oct-22 biancomd [same] moved from PM's mathbox to main set.mm
4-Oct-22 biancomi biancom moved from PM's mathbox to main set.mm
4-Oct-22 dvreslem [same] commutation in theorem
3-Oct-22 brrelexi brrelex1i
3-Oct-22 brrelex brrelex1
1-Oct-22 eu5 dfeu this is now a rederivation
1-Oct-22 mo2v dfmo this is now a rederivation
1-Oct-22 mo2 mof "f-version" of df-mo
26-Sep-22 euequ1 euequ
26-Sep-22 eueq1 eueqi inference associated with eueq
18-Sep-22 brinxp2ALTV brinxp2 moved from PM's mathbox to main set.mm
17-Sep-22 zfnuleu --- deleted; use nulmo instead
17-Sep-22 bm2.5ii uniordint more informative label
17-Sep-22 bm1.1 --- deleted; use axextmo instead
14-Sep-22 idinxpres [same] moved from PM's mathbox to main set.mm
14-Sep-22 relinxp [same] moved from PM's mathbox to main set.mm
14-Sep-22 opelinxp [same] moved from PM's mathbox to main set.mm
14-Sep-22 ralanid [same] moved from PM's mathbox to main set.mm
13-Sep-22 epelc epeli inference associated with epelg
13-Sep-22 a1tru trud deduction form of tru
13-Sep-22 trud mptru modus ponens when minor is tru
8-Sep-22 el2v2 elvd moved from PM's mathbox to main set.mm
8-Sep-22 exlimimdd [same] moved from ML's mathbox to main set.mm
4-Sep-22 funresfunco [same] moved from AV's mathbox to main set.mm
3-Sep-22 pwexd [same] moved from GS's mathbox to main set.mm
3-Sep-22 moimd [same] moved from TA's mathbox to main set.mm
3-Sep-22 csbvargi [same] moved from GM's mathbox to main set.mm
1-Sep-22 keepel ifcli inference associated with ifcl
26-Aug-22 elv [same] moved from PM's mathbox to main set.mm
18-Aug-22 eel1111 syl1111anc moved from AS's mathbox to main set.mm
26-Jul-22 wl-jarri jarri moved from WL's mathbox to main set.mm
26-Jul-22 wl-jarli jarli moved from WL's mathbox to main set.mm
25-Jul-22 bj-sb3b sb3b moved from BJ's mathbox to main set.mm
20-Jul-22 brfi1indlem hashdifsnp1
17-Jul-22 mapsnend [same] moved from GS's mathbox to main set.mm
17-Jul-22 mapsnd [same] moved from GS's mathbox to main set.mm
16-Jul-22 bj-cbv3v2 cbv3v2 moved from mathbox to main
12-Jul-22 equviniva equvinva correct a typo
11-Jul-22 prodge02 --- deleted; use prodge0ld instead
11-Jul-22 prodge0i --- deleted; use prodge0rd instead
11-Jul-22 prodge0 --- deleted; use prodge0rd instead
8-Jul-22 spimvALT spimv shorter, and based on the same set of axioms
6-Jul-22 nfimt bj-nfimt moved to mathbox on request of its owner
6-Jul-22 nfimt2 nfimt nfimt was more difficult to prove and has no
application
5-Jul-22 zrhcopsgndif copsgndif
5-Jul-22 ssrind [same] moved from GS's mathbox to main set.mm
3-Jul-22 zrhcofipsgn cofipsgn
1-Jul-22 bj-1ex 1oex moved from BJ's mathbox to main set.mm
23-Jun-22 rspcda --- deleted; use rspcdva instead
17-May-22 ad5ant1345 adantl3r eliminate duplicated theorem
17-May-22 adantlllr adantl3r eliminate duplicated theorem
21-Apr-22 fz1ssfz0 [same] moved from GS's mathbox to main set.mm
21-Apr-22 rabrab [same] moved from TA's mathbox to main set.mm
8-Mar-22 rabbii [same] moved from PM's mathbox to main set.mm
21-Feb-22 cnvoprab [same] moved from TA's mathbox to main set.mm
16-Feb-22 opidg [same] moved from AV's/PM's mathboxes to main set.mm
5-Feb-22 3orel1 [same] moved from SF's mathbox to main set.mm
5-Feb-22 cofmpt [same] moved from TA's mathbox to main set.mm
27-Jan-22 ccatw2s1cl [same] moved from AV's mathbox to main set.mm
27-Jan-22 fzosplitpr [same] moved from AV's mathbox to main set.mm
23-Jan-22 jca2 [same] moved from RM's mathbox to main set.mm
23-Jan-22 eqvincg [same] moved from TA's mathbox to main set.mm
23-Jan-22 idssxp [same] moved from TA's mathbox to main set.mm
23-Jan-22 dfres3 [same] moved from SF's mathbox to main set.mm
23-Jan-22 brv [same] moved from SF's mathbox to main set.mm
23-Jan-22 dfss6 [same] moved from RP's mathbox to main set.mm
23-Jan-22 2r19.29 [same] moved from RM's mathbox to main set.mm
23-Jan-22 n0el [same] moved from RM's mathbox to main set.mm
19-Jan-22 clelsb3f [same] moved from TA's mathbox to main set.mm
9-Jan-22 sumeq2ad [same] moved from GS's mathbox to main set.mm
3-Jan-22 rabidim1 [same] moved from GS's mathbox to main set.mm
2-Jan-22 xlemnf [same] moved from TA's mathbox to main set.mm
2-Jan-22 infxrmnf [same] moved from TA's mathbox to main set.mm
26-Dec-21 3imp231 [same] moved from AS's mathbox to main set.mm
21-Dec-21 bj-eleq2w eleq2w moved from BJ's mathbox to main set.mm
20-Dec-21 bj-eleq1w eleq1w moved from BJ's mathbox to main set.mm
20-Dec-21 rabeqi [same] moved from GS's mathbox to main set.mm
20-Dec-21 rabeqif [same] moved from GS's mathbox to main set.mm
20-Dec-21 bnj21 ssrab3 moved from JB's mathbox to main set.mm
20-Dec-21 funfnd [same] moved from GS's mathbox to main set.mm
20-Dec-21 elrabd [same] moved from GS's mathbox to main set.mm
20-Dec-21 rabasiun --- deleted; use iunrab instead
19-Dec-21 ssdifsn [same] moved from EW's mathbox to main set.mm
19-Dec-21 dvrecg [same] moved from GS's mathbox to main set.mm
19-Dec-21 dvmptdiv [same] moved from GS's mathbox to main set.mm
16-Dec-21 logge0b & al. [same] moved from AV's mathbox to main set.mm
3-Dec-21 ovexd [same] moved from GS's mathbox to main set.mm
2-Dec-21 divcncf [Same] moved from GS's mathbox to main set.mm
2-Dec-21 mptex2 [Same] moved from GS's mathbox to main set.mm
1-Dec-21 unicntop [Same] moved from GS's mathbox to main set.mm
1-Dec-21 cnopn [Same] moved from GS's mathbox to main set.mm
1-Dec-21 volioo [Same] moved from GS's mathbox to main set.mm
26-Nov-21 fvexd [same] moved from GS's mathbox to main set.mm
26-Nov-21 xgepnf [same] moved from TA's mathbox to main set.mm
26-Nov-21 elnelall [same] moved from AV's mathbox to main set.mm
26-Nov-21 nn0le2is012 [same] moved from AV's mathbox to main set.mm
16-Nov-21 rabbia2 [same] moved from GS's mathbox to main set.mm
16-Nov-21 elpwd [same] moved from GS's mathbox to main set.mm
16-Nov-21 elpwi2 [same] moved from GS's mathbox to main set.mm
16-Nov-21 uhgrstrrepelem setsn0fun split into two theorems
16-Nov-21 uhgrstrrepelem basprssdmsets split into two theorems
14-Nov-21 plusgndxnmulrndx [same] moved from AV's mathbox to main set.mm
14-Nov-21 basendxnmulrndx [same] moved from AV's mathbox to main set.mm
12-Nov-21 --- --- math token "Con" changed to "Conn"
12-Nov-21 --- --- math token "PCon" changed to "PConn"
12-Nov-21 --- --- math token "SCon" changed to "SConn"
12-Nov-21 ccon cconn in labels, "connected" is abbreviated by "conn"
12-Nov-21 df-con df-conn
12-Nov-21 cpcon cpconn
12-Nov-21 df-pcon df-pconn
12-Nov-21 cscon csconn
12-Nov-21 df-scon df-sconn
12-Nov-21 iscon isconn
12-Nov-21 iscon2 isconn2
12-Nov-21 conclo connclo
12-Nov-21 contop conntop
12-Nov-21 indiscon indisconn
12-Nov-21 dfcon2 dfconn2
12-Nov-21 consuba connsuba
12-Nov-21 consub connsub
12-Nov-21 cncon cnconn
12-Nov-21 nconsubb nconnsubb
12-Nov-21 consubclo connsubclo
12-Nov-21 conima connima
12-Nov-21 concn conncn
12-Nov-21 iunconlem iunconnlem
12-Nov-21 iuncon iunconn
12-Nov-21 uncon unconn
12-Nov-21 clscon clsconn
12-Nov-21 concompid conncompid
12-Nov-21 concompcon conncompconn
12-Nov-21 concompss conncompss
12-Nov-21 concompcld conncompcld
12-Nov-21 concompclo conncompclo
12-Nov-21 t1conperf t1connperf
12-Nov-21 txcon txconn
12-Nov-21 qtopcon qtopconn
12-Nov-21 conhmph connhmph
12-Nov-21 filcon filconn
12-Nov-21 tgpconcompeqg tgpconncompeqg
12-Nov-21 tgpconcomp tgpconncomp
12-Nov-21 tgpconcompss tgpconncompss
12-Nov-21 reconlem1 reconnlem1
12-Nov-21 recon reconn
12-Nov-21 retopcon retopconn
12-Nov-21 iicon iiconn
12-Nov-21 xrcon xrconn
12-Nov-21 ordtconlem1 ordtconnlem1
12-Nov-21 ordtcon ordtconn
12-Nov-21 ispcon ispconn
12-Nov-21 pconcn pconncn
12-Nov-21 pcontop pconntop
12-Nov-21 isscon issconn
12-Nov-21 sconpcon sconnpconn
12-Nov-21 scontop sconntop
12-Nov-21 sconpht sconnpht
12-Nov-21 cnpcon cnpconn
12-Nov-21 pconcon pconnconn
12-Nov-21 txpcon txpconn
12-Nov-21 ptpcon ptpconn
12-Nov-21 indispcon indispconn
12-Nov-21 conpcon connpconn
12-Nov-21 qtoppcon qtoppconn
12-Nov-21 pconpi1 pconnpi1
12-Nov-21 sconpht2 sconnpht2
12-Nov-21 sconpi1 sconnpi1
12-Nov-21 txsconlem txsconnlem
12-Nov-21 txscon txsconn
12-Nov-21 cvxpcon cvxpconn
12-Nov-21 cvxscon cvxsconn
12-Nov-21 blscon blsconn
12-Nov-21 cnllyscon cnllysconn
12-Nov-21 rescon resconn
12-Nov-21 iooscon ioosconn
12-Nov-21 iccscon iccsconn
12-Nov-21 retopscon retopsconn
12-Nov-21 iccllyscon iccllysconn
12-Nov-21 rellyscon rellysconn
12-Nov-21 iiscon iisconn
12-Nov-21 iillyscon iillysconn
12-Nov-21 iinllycon iinllyconn
12-Nov-21 onsucconi onsucconni
12-Nov-21 onsuccon onsucconn
12-Nov-21 ordtopcon ordtopconn
12-Nov-21 onintopsscon onintopssconn
12-Nov-21 iunconlem2 iunconnlem2
12-Nov-21 iunconALT iunconnALT
5-Nov-21 fvexi [same] moved from GS's mathbox to main set.mm
2-Nov-21 resunimafz0 [same] moved from AV's mathbox to main set.mm
2-Nov-21 fpropnf1 [same] moved from AV's mathbox to main set.mm
1-Nov-21 f1cofveqaeq [same] moved from AV's mathbox to main set.mm
1-Nov-21 f1cofveqaeqALT [same] moved from AV's mathbox to main set.mm
1-Nov-21 fz0add1fz1 [same] moved from AV's mathbox to main set.mm
31-Oct-21 rexdifpr [same] moved from AV's mathbox to main set.mm
31-Oct-21 pr1eqbg [same] moved from AV's mathbox to main set.mm
31-Oct-21 pr1nebg [same] moved from AV's mathbox to main set.mm
31-Oct-21 2f1fvneq [same] moved from AV's mathbox to main set.mm
31-Oct-21 prinfzo0 [same] moved from AV's mathbox to main set.mm
31-Oct-21 elfzo0l [same] moved from AV's mathbox to main set.mm
31-Oct-21 elfzr [same] moved from AV's mathbox to main set.mm
31-Oct-21 elfzlmr [same] moved from AV's mathbox to main set.mm
31-Oct-21 elfz0lmr [same] moved from AV's mathbox to main set.mm
31-Oct-21 fvmptopab1 fvmptopab revised and renamed
31-Oct-21 fvmptopab2 --- deleted; use fvmptopab instead
31-Oct-21 sylancl3 sylanblrc moved from BJ's mathbox to main set.mm
30-Oct-21 rabid2f [same] moved from TA's mathbox to main set.mm
30-Oct-21 rabtru [same] moved from TA's mathbox to main set.mm
30-Oct-21 mptexgf [same] moved from TA's mathbox to main set.mm
30-Oct-21 suprcld [same] moved from SP's mathbox to main set.mm
30-Oct-21 suprubd [same] moved from SP's mathbox to main set.mm
30-Oct-21 resmptf [same] moved from TA's mathbox to main set.mm
30-Oct-21 fnct [same] moved from TA's mathbox to main set.mm
30-Oct-21 mptct [same] moved from TA's mathbox to main set.mm
30-Oct-21 cnvct [same] moved from TA's mathbox to main set.mm
30-Oct-21 dmct [same] moved from TA's mathbox to main set.mm
30-Oct-21 rnct [same] moved from TA's mathbox to main set.mm
30-Oct-21 mpteq12d [same] moved from SF's mathbox to main set.mm
30-Oct-21 mpteq12df [same] moved from TA's mathbox to main set.mm
26-Oct-21 clel5 [same] moved from AV's mathbox to main set.mm
26-Oct-21 vsssseq [same] moved from AV's mathbox to main set.mm
26-Oct-21 dfss7 dfss5 moved from AV's mathbox to main set.mm
26-Oct-21 n0rex [same] moved from AV's mathbox to main set.mm
26-Oct-21 ssn0rex [same] moved from AV's mathbox to main set.mm
26-Oct-21 ralnralall [same] moved from AV's mathbox to main set.mm
26-Oct-21 falseral0 [same] moved from AV's mathbox to main set.mm
26-Oct-21 elpwdifsn [same] moved from AV's mathbox to main set.mm
26-Oct-21 prcssprc [same] moved from AV's mathbox to main set.mm
26-Oct-21 resresdm [same] moved from AV's mathbox to main set.mm
26-Oct-21 f1ssf1 [same] moved from AV's mathbox to main set.mm
26-Oct-21 riotaeqimp [same] moved from AV's mathbox to main set.mm
26-Oct-21 opabn1stprc [same] moved from AV's mathbox to main set.mm
26-Oct-21 resfnfinfin [same] moved from AV's mathbox to main set.mm
26-Oct-21 residfi [same] moved from AV's mathbox to main set.mm
26-Oct-21 nfile [same] moved from AV's mathbox to main set.mm
26-Oct-21 hash1n0 [same] moved from AV's mathbox to main set.mm
24-Oct-21 ssprss [same] moved from AV's mathbox to main set.mm
24-Oct-21 ssprsseq [same] moved from AV's mathbox to main set.mm
24-Oct-21 issn [same] moved from AV's mathbox to main set.mm
24-Oct-21 n0snor2el [same] moved from AV's mathbox to main set.mm
24-Oct-21 elpr2elpr [same] moved from AV's mathbox to main set.mm
24-Oct-21 prelpw [same] moved from AV's mathbox to main set.mm
24-Oct-21 snopeqop [same] moved from AV's mathbox to main set.mm
24-Oct-21 propeqop [same] moved from AV's mathbox to main set.mm
24-Oct-21 propssopi [same] moved from AV's mathbox to main set.mm
24-Oct-21 iunopeqop [same] moved from AV's mathbox to main set.mm
24-Oct-21 ssrelrn [same] moved from AV's mathbox to main set.mm
24-Oct-21 fun2d [same] moved from AV's mathbox to main set.mm
24-Oct-21 funiun [same] moved from AV's mathbox to main set.mm
24-Oct-21 funopsn [same] moved from AV's mathbox to main set.mm
24-Oct-21 funop [same] moved from AV's mathbox to main set.mm
24-Oct-21 funsndifnop [same] moved from AV's mathbox to main set.mm
24-Oct-21 funsneqopsn [same] moved from AV's mathbox to main set.mm
24-Oct-21 funsneqop [same] moved from AV's mathbox to main set.mm
24-Oct-21 funsneqopb [same] moved from AV's mathbox to main set.mm
24-Oct-21 prprrab [same] moved from AV's mathbox to main set.mm
24-Oct-21 fundmge2nop0 [same] moved from AV's mathbox to main set.mm
24-Oct-21 fundmge2nop [same] moved from AV's mathbox to main set.mm
24-Oct-21 fun2dmnop0 [same] moved from AV's mathbox to main set.mm
24-Oct-21 fun2dmnop [same] moved from AV's mathbox to main set.mm
24-Oct-21 df-xnn0 [same] section "Extended nonnegative integers"
moved from AV's mathbox to main set.mm
20-Oct-21 subdir2d [same] moved from GS's mathbox to main set.mm
9-Oct-21 elini [same] moved from GS's mathbox to main set.mm
7-Oct-21 nfdi nf5di consistent naming
6-Oct-21 bf-nfntht nfntht moved from BJ's mathbox
6-Oct-21 bf-nfntht2 nfntht2 moved from BJ's mathbox
6-Oct-21 nf4 nf3 change the definition of not-free
6-Oct-21 nf3 nf6 change the definition of not-free
6-Oct-21 bj-nf4 nf4 moved from BJ's mathbox
6-Oct-21 bj-nf2 nf2 moved from BJ's mathbox
6-Oct-21 nfrd nf5rd change the definition of not-free
6-Oct-21 nfd nf5d change the definition of not-free
6-Oct-21 nfri nf5ri change the definition of not-free
6-Oct-21 nfi nf5i change the definition of not-free
6-Oct-21 df-nf nf5 change the definition of not-free
6-Oct-21 nf2 df-nf change the definition of not-free
2-Oct-21 adant423 --- deleted; use ad4ant14
21-Sep-21 mptss [same] moved from GS's mathbox to main set.mm
19-Sep-21 ffdmd [same] moved from GS's mathbox to main set.mm
16-Sep-21 csbopg2 csbopg moved from ML's mathbox to main set.mm
15-Sep-21 ovexi [same] moved from GS's mathbox to main set.mm
8-Sep-21 8p2e10b 8p2e10
8-Sep-21 7p3e10b 7p3e10
8-Sep-21 5p5e10b 5p5e10
8-Sep-21 6p4e10b 6p4e10
8-Sep-21 9p1e10b 9p1e10
8-Sep-21 decle [same] moved from AV's mathbox to main set.mm
8-Sep-21 declec decleh moved from AV's mathbox to main set.mm
8-Sep-21 declei [same] moved from AV's mathbox to main set.mm
6-Sep-21 8p2e10b [same] moved from SP's mathbox to main set.mm
6-Sep-21 7p3e10b [same] moved from SP's mathbox to main set.mm
4-Sep-21 5p5e10b [same] moved from SP's mathbox to main set.mm
21-Aug-21 divalgmodcl [same] moved from SO's mathbox to main set.mm
18-Aug-21 3rp [same] moved from GS's mathbox to main set.mm
17-Aug-21 rpennen2 [same] revised - remove unneeded hypothesis
16-Aug-21 bitr3 [same] moved from AS's mathbox to main set.mm
16-Aug-21 eluz2n0 [same] moved from AV's mathbox to main set.mm
15-Aug-21 rpennen1 [same] revised - separate out NN, QQ e. _V as hypoth.
11-Aug-21 crt crth convention: "th" suffix for "theorem"
9-Aug-21 phisum [same] moved from SO's mathbox to main set.mm
9-Aug-21 hashgcdeq [same] moved from SO's mathbox to main set.mm
9-Aug-21 sgmss dvdsssfz1
8-Aug-21 gcdzeq [same] moved from AV's mathbox to main set.mm
7-Aug-21 conss34 conss34OLD use complss instead
7-Aug-21 dvdsleabs2 [same] moved from SO's mathbox to main set.mm
7-Aug-21 2pwp1prm2pw2pwp1prm 2pwp1prm
7-Aug-21 oddprmdvdsn2pw oddprmdvds
6-Aug-21 zoddb --- deleted; use oddm1d2 instead
6-Aug-21 cusgrasizeindslem1 --- deleted; use usgrafilem1 instead
2-Aug-21 nnnfi [same] moved from GS's mathbox to main set.mm
2-Aug-21 addeqxfrd subaddeqd moved from TA's mathbox to main set.mm
2-Aug-21 mvlraddd [same] moved from DAW's mathbox to main set.mm
2-Aug-21 mvrraddd [same] moved from DAW's mathbox to main set.mm
30-Jul-21 muls1d [same] moved from SF's mathbox to main set.mm
30-Jul-21 isprm7 [same] moved from SR's mathbox to main set.mm
30-Jul-21 6p4e10b [same] moved from SP's mathbox to main set.mm
30-Jul-21 9p1e10b [same] moved from SP's mathbox to main set.mm
30-Jul-21 ltsubnn0 [same] moved from AV's mathbox to main set.mm
22-Jul-21 dfss1 --- deleted; use sseqin2
22-Jul-21 dfss5 --- deleted
22-Jul-21 rgenz --- deleted
20-Jul-21 eel0121 mp3an2ani moved from AS's mathbox to main set.mm
20-Jul-21 adddirp1d [same] moved from GS's mathbox to main set.mm
20-Jul-21 prtlem1 jao1i moved from RM's mathbox to main set.mm
17-Jul-21 bezoutr [same] moved from SO's mathbox to main set.mm
17-Jul-21 bezoutr1 [same] moved from SO's mathbox to main set.mm
17-Jul-21 faccld [same] moved from GS's mathbox to main set.mm
17-Jul-21 eqnbrtrd [same] moved from GS's mathbox to main set.mm
17-Jul-21 flltnz [same] moved from GS's mathbox to main set.mm
17-Jul-21 joinlmuladdmuld [same] moved from DAW's mathbox to main set.mm
17-Jul-21 mvrraddi [same] moved from DAW's mathbox to main set.mm
17-Jul-21 usgraexmplvtxlem fz0to4untppr
16-Jul-21 modelico [same] moved from SO's mathbox to main set.mm
16-Jul-21 2txmxeqx [same] moved from AV's mathbox to main set.mm
16-Jul-21 divlt1lt [same] moved from AV's mathbox to main set.mm
16-Jul-21 mod2eq1n2dvds [same] moved from AV's mathbox to main set.mm
16-Jul-21 halfge0 [same] moved from AV's mathbox to main set.mm
17-Jul-21 abtru abv
17-Jul-21 abfal ab0
2-Jul-21 ofccat [same] moved from TA's mathbox to main set.mm
2-Jul-21 ofs2 [same] moved from TA's mathbox to main set.mm
2-Jul-21 ofs1 [same] moved from TA's mathbox to main set.mm
2-Jul-21 ifbieq12d2 [same] moved from TA's mathbox to main set.mm
26-Jun-21 fimact [same] moved from TA's mathbox to main set.mm
26-Jun-21 fimacnvinrn [same] moved from TA's mathbox to main set.mm
26-Jun-21 fimacnvinrn2 [same] moved from TA's mathbox to main set.mm
26-Jun-21 zob [same] moved from AV's mathbox to main set.mm
26-Jun-21 xp1d2m1eqxm1d2 [same] moved from AV's mathbox to main set.mm
8-Jun-21 0in [same] moved from GS's mathbox to main set.mm
4-Jun-21 opelxpd [same] moved from GS's mathbox to main set.mm
4-Jun-21 eluz2gt1 [same] moved from AV's mathbox to main set.mm
2-Jun-21 axc9lem1 ax13lem1 relates rather to ax-13 than axc9
2-Jun-21 axc9lem2 ax13lem2 relates rather to ax-13 than axc9
26-May-21 fzadd2 [same] moved from JM's mathbox to main set.mm
11-May-21 an43 [same] moved from RM's mathbox to main set.mm
11-May-21 an3 [same] moved from RM's mathbox to main set.mm
10-May-21 ffrn [same] moved from GS's mathbox to main set.mm
10-May-21 prtlem90 nelelne moved from RM's mathbox to main set.mm
7-May-21 ee02 mpsylsyld moved from AS's mathbox to main set.mm
4-May-21 hasheqf1oi [same] revised - eliminated unnecessary antecedent
4-May-21 hashf1rn [same] revised - eliminated unnecessary antecedent
3-May-21 elsnc2 elsn2
3-May-21 elsnc2g elsn2g
3-May-21 elsnc elsn
3-May-21 elsncg elsng
3-May-21 elsn velsn
3-May-21 ssnid vsnid
1-May-21 eclclwwlkn0 elqsecl renamed and revised (not depending on walks)
30-Apr-21 exp5l [same] moved from JGH's mathbox to main set.mm
25-Apr-21 ssfid [same] moved from GS's mathbox to main set.mm
23-Apr-21 fvresd [same] moved from GS's mathbox to main set.mm
18-Apr-21 mergeconj bianass moved from GM's mathbox to main set.mm
18-Apr-21 mpteq1i [same] moved from GS's mathbox to main set.mm
18-Apr-21 elabd [same] moved from RP's mathbox to main set.mm
11-Apr-21 equviniv equviniva suffix a: an different, uncommon version
11-Apr-21 equveli equvel consistent naming
11-Apr-21 equvini equvin consistent naming
11-Apr-21 equvin equvinv consistent naming
11-Apr-21 mptexd [same] moved from GS's mathbox to main set.mm
11-Apr-21 fz0hash fnfz0hash
11-Apr-21 hashfzdm ffz0hash
11-Apr-21 hashfirdm fnfzo0hash
8-Apr-21 nnct [same] moved from TA's mathbox to main set.mm
7-Apr-21 fvelimabd [same] moved from SP's mathbox to main set.mm
7-Apr-21 ex3 [same] moved from AS's mathbox to main set.mm
5-Apr-21 adant423 [same] moved from GS's mathbox to main set.mm
5-Apr-21 bnj833 simplbiim moved from JB's mathbox to main set.mm
1-Apr-21 notnot1 notnot
1-Apr-21 notnot2 notnotr
1-Apr-21 notnot notnotb
31-Mar-21 bj-animorl animorl moved from BJ's mathbox to main set.mm
31-Mar-21 bj-animorr animorr moved from BJ's mathbox to main set.mm
31-Mar-21 bj-animorlr animorlr moved from BJ's mathbox to main set.mm
31-Mar-21 bj-animorrl animorrl moved from BJ's mathbox to main set.mm
31-Mar-21 a1i13 [same] moved from JGH's mathbox to main set.mm
28-Mar-21 hypstkd mpidan renamed to match similar theorems
25-Mar-21 difex difexi moved from GS's mathbox to main set.mm
25-Mar-21 mpbirand [same] moved from GS's mathbox to main set.mm
22-Mar-21 ffund [same] moved from GS's mathbox to main set.mm
24-Mar-21 wl-ax12v1 ax12v moved from WL's mathbox to main set.mm
24-Mar-21 wl-ax12v2 ax12v2 moved from WL's mathbox to main set.mm
24-Mar-21 axc112 axc11r consistent naming style
24-Mar-21 wl-ax12v3 axc15 moved from WL's mathbox to main set.mm
24-Mar-21 wl-ax12 ax12 moved from WL's mathbox to main set.mm
23-Mar-21 aevlem1 aevlem
22-Mar-21 dummylink a1ii dummylink kept to prevent broken links
20-Mar-21 eluzmn [same] moved from TA's mathbox to main set.mm
20-Mar-21 biimpa21 --- deleted; duplicate of biimpac
20-Mar-21 lt2addmuld [same] moved from GS's mathbox to main set.mm
20-Mar-21 possumd [same] moved from SF's mathbox to main set.mm
20-Mar-21 comraddd [same] moved from DAW's mathbox to main set.mm
20-Mar-21 eel2221 syl2an23an moved from AS's mathbox to main set.mm
20-Mar-21 ltaddneg [same] moved from GS's mathbox to main set.mm
20-Mar-21 lelttrdi [same] moved from AV's mathbox to main set.mm
20-Mar-21 ralxfrd2 [same] moved from AV's mathbox to main set.mm
20-Mar-21 rexxfrd2 [same] moved from AV's mathbox to main set.mm
19-Mar-21 speqv spaev consistent naming
16-Mar-21 con3th con3ALT
8-Mar-21 iatbtatnnb notnotd moved from JU's mathbox to main set.mm
8-Mar-21 f1oeq3d [same] moved from GS's mathbox to main set.mm
8-Mar-21 fimass [same] moved from GS's mathbox to main set.mm
8-Mar-21 rspcdva [same] moved from TA's mathbox to main set.mm
8-Mar-21 rspcda [same] moved from TA's mathbox to main set.mm
8-Mar-21 xaddid1d [same] moved from GS's mathbox to main set.mm
8-Mar-21 AnelBC prneli moved from DAW's mathbox to main set.mm
8-Mar-21 eel012 mp3an3an moved from AS's mathbox to main set.mm
3-Mar-21 iunxprg [same] moved from AV's mathbox to main set.mm
3-Mar-21 sselpwd [same] moved from TA's mathbox to main set.mm
3-Mar-21 dfrel4 [same] moved from TA's mathbox to main set.mm
3-Mar-21 feqmptdf [same] moved from TA's mathbox to main set.mm
3-Mar-21 unidmvol [same] moved from TA's mathbox to main set.mm
3-Mar-21 xrge0nre [same] moved from TA's mathbox to main set.mm
3-Mar-21 iunxdif3 [same] moved from TA's mathbox to main set.mm
26-Feb-21 rprssd [same] moved from GS's mathbox to main set.mm
24-Feb-21 rexaddd [same] moved from GS's mathbox to main set.mm
24-Feb-21 rabeqd rabeqdv moved from GS's mathbox to main set.mm
14-Feb-21 bj-pm2.18i pm2.18i moved from BJ's mathbox to main set.mm
14-Feb-21 3imp31 [same] moved from AS's mathbox to main set.mm
14-Feb-21 eel32131 3imp3i2an moved from AS's mathbox to main set.mm
14-Feb-21 eel011 mp3an2i moved from AS's mathbox to main set.mm
31-Jan-21 isprmpt2 rbropapd
30-Jan-21 neqne [same] moved from GS's mathbox to main set.mm
30-Jan-21 sylbbr [same] moved from BJ's mathbox to main set.mm
30-Jan-21 sylbb1 [same] moved from BJ's mathbox to main set.mm
30-Jan-21 sylbb2 [same] moved from BJ's mathbox to main set.mm
25-Jan-21 hypstkd [same] moved from SP's mathbox to main set.mm
25-Jan-21 eel112 syl2an3an moved from AS's mathbox to main set.mm
16-Jan-21 prtlem50 anim12d1 moved from RM's mathbox to main set.mm
6-Jan-21 3imp21 [same] moved from AS's mathbox to main set.mm
3-Jan-21 elexd [same] moved from GS's mathbox to main set.mm
3-Jan-21 fz1fzo0m1 [same] moved from TA's mathbox to main set.mm
28-Dec-20 ceqsexv2d [same] moved from TA's mathbox to main set.mm
25-Dec-20 icodiamlt [same] moved from SO's mathbox to main set.mm
25-Dec-20 fict [same] moved from TA's mathbox to main set.mm
25-Dec-20 ctex [same] moved from TA's mathbox to main set.mm
25-Dec-20 xpct [same] moved from TA's mathbox to main set.mm
25-Dec-20 ssct [same] moved from TA's mathbox to main set.mm
25-Dec-20 regsumfsum [same] moved from TA's mathbox to main set.mm
25-Dec-20 elin1d [same] moved from TA's mathbox to main set.mm
25-Dec-20 elin2d [same] moved from TA's mathbox to main set.mm
18-Dec-20 preqsnd [same] moved from TA's mathbox to main set.mm
18-Dec-20 rabeqsn [same] moved from AV's mathbox to main set.mm
18-Dec-20 rabsssn [same] moved from AV's mathbox to main set.mm
18-Dec-20 eel001 mp3an12i moved from AS's mathbox to main set.mm
17-Dec-20 eel121 syl2an2r moved from AS's mathbox to main set.mm
12-Dec-20 ffnd [same] moved from GS's mathbox to main set.mm
8-Nov-20 prcnel [same] moved from GS's mathbox to main set.mm
8-Nov-20 nelsn [same] moved from GS's mathbox to main set.mm
28-Oct-20 rmoeq [same] moved from TA's mathbox to main set.mm
23-Oct-20 usgraexvlem usgraexmplvtxlem
19-Oct-20 usgrnloop usgrnwlkloop
18-Oct-20 bj-equsalvv equsalvw moved from BJ's mathbox to main set.mm
11-Oct-20 ishashinf [same] moved from TA's mathbox to main set.mm
11-Oct-20 xrge0neqmnf[same] moved from TA's mathbox to main set.mm
11-Oct-20 elsnxp [same] moved from TA's mathbox to main set.mm
11-Oct-20 nn0rp0 [same] moved from AV's mathbox to main set.mm
13-Sep-20 infmxrss infxrss moved from GS's mathbox to main set.mm
13-Sep-20 reltre [same] moved from AV's mathbox to main set.mm
13-Sep-20 rpltrp [same] moved from AV's mathbox to main set.mm
13-Sep-20 reltxrnmnf [same] moved from AV's mathbox to main set.mm
13-Sep-20 infmremnf [same] moved from AV's mathbox to main set.mm
13-Sep-20 infmrp1 [same] moved from AV's mathbox to main set.mm
11-Sep-20 xrinfm0 xrinf0
11-Sep-20 infmxrre infxrre
11-Sep-20 infmxrgelb infxrgelb
11-Sep-20 infmxrlb infxrlb
11-Sep-20 infmxrcl infxrcl
11-Sep-20 infmssuzcl infssuzcl
11-Sep-20 infmssuzle infssuzle
11-Sep-20 nn0infm nn0inf
11-Sep-20 nninfm nninf
11-Sep-20 uzinfmi uzinfi
11-Sep-20 infmrlb infrelb
11-Sep-20 infmrgelb infregelb
11-Sep-20 infmsup infrenegsup
11-Sep-20 infmrcl infrecl
11-Sep-20 dfinfmr dfinfre
11-Sep-20 lbinfmle lbinfle
11-Sep-20 lbinfmcl lbinfcl
11-Sep-20 lbinfm lbinf
11-Sep-20 df-inf [same] moved together with related theorems
from AV's mathbox to main set.mm
8-Sep-20 ax16g-o axc16g-o
8-Sep-20 ax16gb axc16gb
8-Sep-20 ax16nf axc16nf
8-Sep-20 ax16nfALT axc16nfALT
5-Sep-20 mnfltd [same] moved from GS's mathbox to main set.mm
5-Sep-20 xrletri4 xrletrid moved from GS's mathbox to main set.mm
5-Sep-20 xrlenltd [same] moved from GS's mathbox to main set.mm
27-Aug-20 df-lcm [same] moved together with related theorems
from SR's mathbox to main set.mm
27-Aug-20 fzssz [same] moved from GS's mathbox to main set.mm
27-Aug-20 impel [same] moved from GM's mathbox to main set.mm
27-Aug-20 exp5j [same] moved from JGH's mathbox to main set.mm
27-Aug-20 eel221 syl2an2 moved from AS's mathbox to main set.mm
22-Aug-20 bj-disjdif disjdif2 moved from BJ's mathbox to main set.mm
19-Aug-20 fprodsplitsn [same] moved from GS's mathbox to main set.mm
19-Aug-20 prodsnf [same] moved from GS's mathbox to main set.mm
19-Aug-20 elunnel1 [same] moved from GS's mathbox to main set.mm
19-Aug-20 fzssnn [same] moved from TA's mathbox to main set.mm
17-Aug-20 supaddc [same] moved from BL's mathbox to main set.mm
17-Aug-20 supadd [same] moved from BL's mathbox to main set.mm
17-Aug-20 inisegn0 [same] moved from SO's mathbox to main set.mm
17-Aug-20 ad4ant13 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad4ant14 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad4ant123 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad4ant124 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad4ant134 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad4ant23 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad4ant24 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad4ant234 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant12 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant13 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant14 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant15 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant23 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant24 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant25 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant245 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant234 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant235 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant123 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant124 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant125 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant134 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant135 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant145 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant1345 [same] moved from AS's mathbox to main set.mm
17-Aug-20 ad5ant2345 [same] moved from AS's mathbox to main set.mm
16-Aug-20 fprodeq0g [same] moved from GS's mathbox to main set.mm
16-Aug-20 fprodle [same] moved from GS's mathbox to main set.mm
16-Aug-20 fproddivf [same] moved from GS's mathbox to main set.mm
16-Aug-20 fprodreclf [same] moved from GS's mathbox to main set.mm
16-Aug-20 fprodclf [same] moved from GS's mathbox to main set.mm
16-Aug-20 fprodsplit1f [same] moved from GS's mathbox to main set.mm
16-Aug-20 fprodsplitf [same] moved from GS's mathbox to main set.mm
16-Aug-20 fprodsplit [same] moved from GS's mathbox to main set.mm
16-Aug-20 fprodcllemf [same] moved from GS's mathbox to main set.mm
16-Aug-20 fprodge1 [same] moved from GS's mathbox to main set.mm
16-Aug-20 fprodge0 [same] moved from GS's mathbox to main set.mm
16-Aug-20 fprodn0f [same] moved from GS's mathbox to main set.mm
16-Aug-20 prodsns [same] moved from GS's mathbox to main set.mm
16-Aug-20 icogelb [same] moved from GS's mathbox to main set.mm
16-Aug-20 leneltd [same] moved from GS's mathbox to main set.mm
16-Aug-20 ltpnfd [same] moved from GS's mathbox to main set.mm
16-Aug-20 divge1 [same] moved from GS's mathbox to main set.mm
16-Aug-20 elicod [same] moved from GS's mathbox to main set.mm
16-Aug-20 neneq [same] moved from GS's mathbox to main set.mm
16-Aug-20 f1dmvrnfibi [same] moved from AV's mathbox to main set.mm
16-Aug-20 f1vrnfibi [same] moved from AV's mathbox to main set.mm
16-Aug-20 fundmfibi [same] moved from AV's mathbox to main set.mm
16-Aug-20 prmssnn [same] moved from AV's mathbox to main set.mm
16-Aug-20 prmex [same] moved from AV's mathbox to main set.mm
16-Aug-20 gcdnncl [same] moved from TA's mathbox to main set.mm
9-Aug-20 a1ii 2a1i
9-Aug-20 a1dd2 2a1dd
7-Aug-20 bi3 impbi
7-Aug-20 bi2 biimpr
7-Aug-20 bi1 biimp
2-Aug-20 --- --- definition "TarskiG2D" moved to TA's mathbox
2-Aug-20 elicore [same] moved from GS's mathbox to main set.mm
2-Aug-20 simplrd [same] moved from GS's mathbox to main set.mm
2-Aug-20 simprld [same] moved from GS's mathbox to main set.mm
26-Jul-20 sumpr [same] moved from TA's mathbox to main set.mm
22-Jul-20 ifpor [same] moved from BJ's mathbox to main set.mm
19-Jul-20 xrnltled [same] moved from GS's mathbox to main set.mm
18-Jul-20 lensymd [same] moved from GS's mathbox to main set.mm
18-Jul-20 sublt0d [same] moved from GS's mathbox to main set.mm
18-Jul-20 offval2f [same] moved from TA's mathbox to main set.mm
18-Jul-20 nltled [same] moved from GS's mathbox to main set.mm
18-Jul-20 eqled [same] moved from GS's mathbox to main set.mm
18-Jul-20 elinel2 [same] moved from GS's mathbox to main set.mm
18-Jul-20 elinel1 [same] moved from GS's mathbox to main set.mm
18-Jul-20 dvcnsqrt [same] moved from BL's mathbox to main set.mm
18-Jul-20 dvcncxp1 [same] moved from BL's mathbox to main set.mm
18-Jul-20 divcnvshft [same] moved from SF's mathbox to main set.mm
18-Jul-20 syldanl [same] moved from JM's mathbox to main set.mm
18-Jul-20 czeta [same] moved from MC's mathbox to main set.mm
18-Jul-20 df-zeta [same] moved from MC's mathbox to main set.mm
18-Jul-20 clgam [same] moved from MC's mathbox to main set.mm
18-Jul-20 cgam [same] moved from MC's mathbox to main set.mm
18-Jul-20 cigam [same] moved from MC's mathbox to main set.mm
18-Jul-20 df-lgam [same] moved from MC's mathbox to main set.mm
18-Jul-20 df-gam [same] moved from MC's mathbox to main set.mm
18-Jul-20 df-igam [same] moved from MC's mathbox to main set.mm
18-Jul-20 zetacvg [same] moved from MC's mathbox to main set.mm
18-Jul-20 eldmgm [same] moved from MC's mathbox to main set.mm
18-Jul-20 dmgmaddn0 [same] moved from MC's mathbox to main set.mm
18-Jul-20 dmlogdmgm [same] moved from MC's mathbox to main set.mm
18-Jul-20 rpdmgm [same] moved from MC's mathbox to main set.mm
18-Jul-20 dmgmn0 [same] moved from MC's mathbox to main set.mm
18-Jul-20 dmgmaddnn0 [same] moved from MC's mathbox to main set.mm
18-Jul-20 dmgmdivn0 [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgamgulmlem1 [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgamgulmlem2 [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgamgulmlem3 [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgamgulmlem4 [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgamgulmlem5 [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgamgulmlem6 [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgamgulm [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgamgulm2 [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgambdd [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgamucov [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgamucov2 [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgamcvglem [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgamcl [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgamf [same] moved from MC's mathbox to main set.mm
18-Jul-20 gamf [same] moved from MC's mathbox to main set.mm
18-Jul-20 gamcl [same] moved from MC's mathbox to main set.mm
18-Jul-20 eflgam [same] moved from MC's mathbox to main set.mm
18-Jul-20 gamne0 [same] moved from MC's mathbox to main set.mm
18-Jul-20 igamval [same] moved from MC's mathbox to main set.mm
18-Jul-20 igamz [same] moved from MC's mathbox to main set.mm
18-Jul-20 igamgam [same] moved from MC's mathbox to main set.mm
18-Jul-20 igamlgam [same] moved from MC's mathbox to main set.mm
18-Jul-20 igamf [same] moved from MC's mathbox to main set.mm
18-Jul-20 igamcl [same] moved from MC's mathbox to main set.mm
18-Jul-20 gamigam [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgamcvg [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgamcvg2 [same] moved from MC's mathbox to main set.mm
18-Jul-20 gamcvg [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgamp1 [same] moved from MC's mathbox to main set.mm
18-Jul-20 gamp1 [same] moved from MC's mathbox to main set.mm
18-Jul-20 gamcvg2lem [same] moved from MC's mathbox to main set.mm
18-Jul-20 gamcvg2 [same] moved from MC's mathbox to main set.mm
18-Jul-20 regamcl [same] moved from MC's mathbox to main set.mm
18-Jul-20 relgamcl [same] moved from MC's mathbox to main set.mm
18-Jul-20 rpgamcl [same] moved from MC's mathbox to main set.mm
18-Jul-20 lgam1 [same] moved from MC's mathbox to main set.mm
18-Jul-20 gam1 [same] moved from MC's mathbox to main set.mm
18-Jul-20 facgam [same] moved from MC's mathbox to main set.mm
18-Jul-20 gamfac [same] moved from MC's mathbox to main set.mm
18-Jul-20 m1expevenALT m1expeven moved from SF's mathbox to main set.mm
18-Jul-20 fallfacfac [same] moved from SF's mathbox to main set.mm
18-Jul-20 bcfallfac [same] moved from SF's mathbox to main set.mm
18-Jul-20 fallfacval4 [same] moved from SF's mathbox to main set.mm
18-Jul-20 binomrisefac [same] moved from SF's mathbox to main set.mm
18-Jul-20 binomfallfac [same] moved from SF's mathbox to main set.mm
18-Jul-20 binomfallfaclem2 [same] moved from SF's mathbox to main set.mm
18-Jul-20 binomfallfaclem1 [same] moved from SF's mathbox to main set.mm
18-Jul-20 0risefac [same] moved from SF's mathbox to main set.mm
18-Jul-20 0fallfac [same] moved from SF's mathbox to main set.mm
18-Jul-20 fallfacfwd [same] moved from SF's mathbox to main set.mm
18-Jul-20 risefacfac [same] moved from SF's mathbox to main set.mm
18-Jul-20 fallfac1 [same] moved from SF's mathbox to main set.mm
18-Jul-20 risefac1 [same] moved from SF's mathbox to main set.mm
18-Jul-20 fallfacp1d [same] moved from SF's mathbox to main set.mm
18-Jul-20 risefacp1d [same] moved from SF's mathbox to main set.mm
18-Jul-20 fallfacp1 [same] moved from SF's mathbox to main set.mm
18-Jul-20 risefacp1 [same] moved from SF's mathbox to main set.mm
18-Jul-20 fallfac0 [same] moved from SF's mathbox to main set.mm
18-Jul-20 risefac0 [same] moved from SF's mathbox to main set.mm
18-Jul-20 risefall0lem [same] moved from SF's mathbox to main set.mm
18-Jul-20 fallrisefac [same] moved from SF's mathbox to main set.mm
18-Jul-20 risefallfac [same] moved from SF's mathbox to main set.mm
18-Jul-20 rprisefaccl [same] moved from SF's mathbox to main set.mm
18-Jul-20 nn0risefaccl [same] moved from SF's mathbox to main set.mm
18-Jul-20 zfallfaccl [same] moved from SF's mathbox to main set.mm
18-Jul-20 zrisefaccl [same] moved from SF's mathbox to main set.mm
18-Jul-20 nnrisefaccl [same] moved from SF's mathbox to main set.mm
18-Jul-20 refallfaccl [same] moved from SF's mathbox to main set.mm
18-Jul-20 rerisefaccl [same] moved from SF's mathbox to main set.mm
18-Jul-20 fallfaccl [same] moved from SF's mathbox to main set.mm
18-Jul-20 risefaccl [same] moved from SF's mathbox to main set.mm
18-Jul-20 fallfaccllem [same] moved from SF's mathbox to main set.mm
18-Jul-20 risefaccllem [same] moved from SF's mathbox to main set.mm
18-Jul-20 fallfacval3 [same] moved from SF's mathbox to main set.mm
18-Jul-20 fallfacval2 [same] moved from SF's mathbox to main set.mm
18-Jul-20 risefacval2 [same] moved from SF's mathbox to main set.mm
18-Jul-20 fallfacval [same] moved from SF's mathbox to main set.mm
18-Jul-20 risefacval [same] moved from SF's mathbox to main set.mm
18-Jul-20 df-fallfac [same] moved from SF's mathbox to main set.mm
18-Jul-20 df-risefac [same] moved from SF's mathbox to main set.mm
18-Jul-20 crisefac [same] moved from SF's mathbox to main set.mm
18-Jul-20 cfallfac [same] moved from SF's mathbox to main set.mm
18-Jul-20 m1expeven --- deleted; use more general m1expevenALT
18-Jul-20 anifp [same] moved from BJ's mathbox to main set.mm
18-Jul-20 dfid6 [same] moved from RP's mathbox to main set.mm
18-Jul-20 dfid5 [same] moved from RP's mathbox to main set.mm
18-Jul-20 dfid4 [same] moved from SF's mathbox to main set.mm
18-Jul-20 abeq2f [same] moved from TA's mathbox to main set.mm
18-Jul-20 fvmpt2f [same] moved from TA's mathbox to main set.mm
18-Jul-20 mptfnf [same] moved from TA's mathbox to main set.mm
18-Jul-20 fnmptf [same] moved from TA's mathbox to main set.mm
18-Jul-20 fmpt3d [same] moved from TA's mathbox to main set.mm
18-Jul-20 cbvmptf [same] moved from TA's mathbox to main set.mm
18-Jul-20 negelrp [same] moved from TA's mathbox to main set.mm
18-Jul-20 mul2lt0rlt0 [same] moved from TA's mathbox to main set.mm
18-Jul-20 mul2lt0rgt0 [same] moved from TA's mathbox to main set.mm
18-Jul-20 mul2lt0llt0 [same] moved from TA's mathbox to main set.mm
18-Jul-20 mul2lt0lgt0 [same] moved from TA's mathbox to main set.mm
18-Jul-20 mul2lt0bi [same] moved from TA's mathbox to main set.mm
18-Jul-20 difneqnul difn0 moved from TA's mathbox to main set.mm
18-Jul-20 3impexp [same] moved from AS's mathbox to main set.mm
18-Jul-20 a1i34 a1dd2 moved from JGH's mathbox to main set.mm
18-Jul-20 a1i4 a1ddd moved from JGH's mathbox to main set.mm
12-Jul-20 ralnex2 [same] moved from GS's mathbox to main set.mm
10-Jul-20 [many] [same] ax-7d through ax-11d moved from main set.mm to
MC's mathbox
10-Jul-20 ax-meredith [same] Moved from main set.mm to NM's mathbox
10-Jul-20 [many] [same] ax-c5 through axc11-o moved from main set.mm to
NM's mathbox
7-Jul-20 modidmul0 mulmod0
27-Jun-20 swrdsymbeq --- deleted; use swrdeq instead
25-Jun-20 r19.29_2a r19.29vva
25-Jun-20 tghilbert1_2 tghilberti2
25-Jun-20 tghilbert1_1 tghilberti1
21-Jun-20 rtrclreclem.refl rtrclreclem1
21-Jun-20 rtrclreclem.subset rtrclreclem2
21-Jun-20 rtrclreclem.trans rtrclreclem3
21-Jun-20 rtrclreclem.min rtrclreclem4
11-Jun-20 rnlogbcl relogbcl
11-Jun-20 rnlogbval relogbval
11-Jun-20 relogbcl relogbzcl
11-Jun-20 relogbcxp [same] moved from AV's mathbox to main set.mm
11-Jun-20 cxplogb [same] moved from AV's mathbox to main set.mm
9-Jun-20 logbleb [same] moved from AV's mathbox to main set.mm
9-Jun-20 relogbmulexp [same] moved from AV's mathbox to main set.mm
9-Jun-20 relogbmul [same] moved from AV's mathbox to main set.mm
9-Jun-20 relogbdiv [same] moved from AV's mathbox to main set.mm
9-Jun-20 rpcndif0 [same] moved from AV's mathbox to main set.mm
9-Jun-20 df-logb [same] section "Logarithm laws generalized to an
arbitrary base" moved from TA's mathbox to main
set.mm
9-Jun-20 rnlogblem zgt1rpn0n1 moved from TA's mathbox to main set.mm
7-Jun-20 znnn0nn [same] moved from GS's mathbox to main set.mm
7-Jun-20 bj-lsub addlsub moved from BJ's mathbox to main set.mm
7-Jun-20 bj-rsub addrsub moved from BJ's mathbox to main set.mm
7-Jun-20 bj-msub subexsub moved from BJ's mathbox to main set.mm
7-Jun-20 bj-flbi3 ico01fl0 moved from BJ's mathbox to main set.mm
5-Jun-20 coss12d [same] moved from RP's mathbox to main set.mm
5-Jun-20 trrelssd [same] moved from RP's mathbox to main set.mm
5-Jun-20 xpcogend [same] moved from RP's mathbox to main set.mm
5-Jun-20 xpcoidgend [same] moved from RP's mathbox to main set.mm
5-Jun-20 cotr2g [same] moved from RP's mathbox to main set.mm
5-Jun-20 cotr2 [same] moved from RP's mathbox to main set.mm
5-Jun-20 cotr3 [same] moved from RP's mathbox to main set.mm
5-Jun-20 coemptyd [same] moved from RP's mathbox to main set.mm
5-Jun-20 xptrrel [same] moved from RP's mathbox to main set.mm
5-Jun-20 0trrel [same] moved from RP's mathbox to main set.mm
5-Jun-20 cleq1lem [same] moved from RP's mathbox to main set.mm
5-Jun-20 cleq1 [same] moved from RP's mathbox to main set.mm
5-Jun-20 clsslem [same] moved from RP's mathbox to main set.mm
5-Jun-20 ctcl [same] section "Transitive closure" moved from Guides
and Miscellanea to main set.mm
5-Jun-20 crtcl [same] section "Transitive closure" moved from Guides
and Miscellanea to main set.mm
5-Jun-20 df-trcl [same] section "Transitive closure" moved from Guides
and Miscellanea to main set.mm
5-Jun-20 df-rtrcl [same] section "Transitive closure" moved from Guides
and Miscellanea to main set.mm
5-Jun-20 trcleq1 [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclsslem [same] moved from RP's mathbox to main set.mm
5-Jun-20 trcleq2lem [same] moved from RP's mathbox to main set.mm
5-Jun-20 cvbtrcl [same] moved from RP's mathbox to main set.mm
5-Jun-20 trcleq12lem [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclexlem [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclublem [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclubi [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclubgi [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclub [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclubg [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclfv [same] moved from RP's mathbox to main set.mm
5-Jun-20 brintclab [same] moved from RP's mathbox to main set.mm
5-Jun-20 brtrclfv [same] moved from RP's mathbox to main set.mm
5-Jun-20 brcnvtrclfv [same] moved from RP's mathbox to main set.mm
5-Jun-20 brtrclfvcnv [same] moved from RP's mathbox to main set.mm
5-Jun-20 brcnvtrclfvcnv [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclfvss [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclfvub [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclfvlb [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclfvcotr [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclfvlb2 [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclfvlb3 [same] moved from RP's mathbox to main set.mm
5-Jun-20 cotrtrclfv [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclidm [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclun [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclfvg [same] moved from RP's mathbox to main set.mm
5-Jun-20 trclfvcotrg [same] moved from RP's mathbox to main set.mm
5-Jun-20 reltrclfv [same] moved from RP's mathbox to main set.mm
5-Jun-20 dmtrclfv [same] moved from RP's mathbox to main set.mm
5-Jun-20 crelexp [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 df-relexp [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexp0g [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexp0 [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexp0d [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpsucnnr [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexp1g [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpsucr [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpsucrd [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexp1d [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpsucnnl [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpsucl [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpsucld [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpcnv [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpcnvd [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexp0rel [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexprelg [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexprel [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpreld [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpnndm [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpdmg [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpdm [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpdmd [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpnnrn [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexprng [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexprn [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexprnd [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpfld [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpfldd [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpaddnn [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpuzrel [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpaddg [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpaddd [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 crtrcl [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 df-rtrclrec [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 dfrtrclrec2 [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 rtrclreclem.refl [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 rtrclreclem.subset [same] moved from Drahflow's mathbox to main
set.mm
5-Jun-20 rtrclreclem.trans [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 rtrclreclem.min [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 dfrtrcl2 [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpindlem [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 relexpind [same] moved from Drahflow's mathbox to main set.mm
5-Jun-20 rtrclind [same] moved from Drahflow's mathbox to main set.mm
31-May-20 rp-isfinite4 isfinite4 moved from RP's mathbox to main set.mm
24-May-20 fz1ssnn --- moved from SO's mathbox to main set.mm
21-May-20 --- --- section "The category of extensible structures"
moved from AV's mathbox to main set.mm
21-May-20 --- --- section "Initial, terminal and zero objects of
a category" moved from AV's mathbox to main
set.mm
21-May-20 --- --- section "Isomorphic objects" moved from AV's
mathbox to main set.mm
21-May-20 invisoinvl [same] moved from AV's mathbox to main set.mm
21-May-20 invisoinvr [same] moved from AV's mathbox to main set.mm
21-May-20 invcoisoid [same] moved from AV's mathbox to main set.mm
21-May-20 isocoinvid [same] moved from AV's mathbox to main set.mm
21-May-20 sectid [same] moved from AV's mathbox to main set.mm
21-May-20 invid [same] moved from AV's mathbox to main set.mm
21-May-20 idiso [same] moved from AV's mathbox to main set.mm
21-May-20 idinv [same] moved from AV's mathbox to main set.mm
21-May-20 isofn [same] moved from AV's mathbox to main set.mm
21-May-20 isofval [same] moved from AV's mathbox to main set.mm
21-May-20 dfiso3 [same] moved from AV's mathbox to main set.mm
21-May-20 dfiso2 [same] moved from AV's mathbox to main set.mm
21-May-20 inveq [same] moved from AV's mathbox to main set.mm
21-May-20 fnhomeqhomf [same] moved from AV's mathbox to main set.mm
21-May-20 slotsbhcdif [same] moved from AV's mathbox to main set.mm
21-May-20 1strstr [same] moved from AV's mathbox to main set.mm
21-May-20 1strbas [same] moved from AV's mathbox to main set.mm
21-May-20 1strwunbndx [same] moved from AV's mathbox to main set.mm
21-May-20 1strwun [same] moved from AV's mathbox to main set.mm
21-May-20 ressval3d [same] moved from AV's mathbox to main set.mm
21-May-20 setsidvald [same] moved from AV's mathbox to main set.mm
21-May-20 strndxid [same] moved from AV's mathbox to main set.mm
21-May-20 rcaninv [same] moved from AV's mathbox to main set.mm
21-May-20 tpres [same] moved from AV's mathbox to main set.mm
21-May-20 mptrcl [same] moved from AV's mathbox to main set.mm
21-May-20 euelss [same] moved from AV's mathbox to main set.mm
8-May-20 wrdeqswrdlsw --- deleted; duplicate of 2swrd1eqwrdeq
2-May-20 swrdvalodm swrdnd2
2-May-20 swrdvalodm2 --- deleted; duplicate of swrdnd
2-May-20 mptrel [same] moved from SF's mathbox to main set.mm
2-May-20 iswrdbi iswrdb
26-Apr-20 --- --- math token "(++)" changed to "/_\"
12-Apr-20 r19.27av r19.27v
12-Apr-20 r19.28av r19.28v
12-Apr-20 r19.36av r19.36v
12-Apr-20 r19.37av r19.37v
12-Apr-20 r19.44av r19.44v
12-Apr-20 r19.45av r19.45v
12-Apr-20 19.36aiv 19.36iv
12-Apr-20 19.37aiv 19.37iv
5-Apr-20 nn0indd [same] moved from TA's mathbox to main set.mm
5-Apr-20 dgrnznn [same] moved from SO's mathbox to main set.mm
31-Mar-20 pnpncand [same] moved from SF's mathbox to main set.mm
31-Mar-20 fzp1nel [same] moved from SF's mathbox to main set.mm
31-Mar-20 prodf [same] moved from SF's mathbox to main set.mm
31-Mar-20 clim2prod [same] moved from SF's mathbox to main set.mm
31-Mar-20 clim2div [same] moved from SF's mathbox to main set.mm
31-Mar-20 prodfmul [same] moved from SF's mathbox to main set.mm
31-Mar-20 prodf1 [same] moved from SF's mathbox to main set.mm
31-Mar-20 prodf1f [same] moved from SF's mathbox to main set.mm
31-Mar-20 prodfclim1 [same] moved from SF's mathbox to main set.mm
31-Mar-20 prodfn0 [same] moved from SF's mathbox to main set.mm