{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":35487449,"defaultBranch":"develop","name":"set.mm","ownerLogin":"metamath","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2015-05-12T12:48:55.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/5435286?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1714941530.0","currentOid":""},"activityList":{"items":[{"before":"014b82e699fc09cb32ca6dd7ac468c7d087b0002","after":"b7e573b6c7a7777f09a3ccbe1ff37a3e822c808c","ref":"refs/heads/develop","pushedAt":"2024-05-06T11:23:59.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"wlammen","name":"Wolf Lammen","path":"/wlammen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30736367?s=80&v=4"},"commit":{"message":"zeroes and inverses (ax-mulcom pr 6) (#3975)\n\n* zeroes and inverses (ax-mulcom pr 6)\r\n\r\nmain results:\r\n+ resubeqsub\r\n+ sn-addid1\r\n+ sn-mul01\r\n\r\n--- comment\r\n\r\nnow almost every important fact about 0 is known, except 0a = 0\r\n\r\nthe eqtrd and eqtr3d in sn-addid0 could be combined probably; an auto-minimize idea for future me\r\n\r\n* typos, addcan2d\r\n\r\n* shorten reixi\r\n\r\n* shorten sn-addid0 (last commit)","shortMessageHtmlLink":"zeroes and inverses (ax-mulcom pr 6) (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2279683779\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3975\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3975/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3975\">#3975</a>)"}},{"before":"763f3329c24e41b80fde444fda5143d4eb40412c","after":"014b82e699fc09cb32ca6dd7ac468c7d087b0002","ref":"refs/heads/develop","pushedAt":"2024-05-05T20:45:05.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"tirix","name":null,"path":"/tirix","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5831830?s=80&v=4"},"commit":{"message":"shorten ifpn (#3974)\n\n* shorten ifpn\r\n\r\n* discouraged","shortMessageHtmlLink":"shorten ifpn (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2279368142\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3974\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3974/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3974\">#3974</a>)"}},{"before":"a089eb1d252a9caba92a95e6845a76c11be2696d","after":null,"ref":"refs/heads/definiton","pushedAt":"2024-05-05T20:38:50.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"tirix","name":null,"path":"/tirix","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5831830?s=80&v=4"}},{"before":"040ac00ee62b706ea921bcf09db27c921f664158","after":"763f3329c24e41b80fde444fda5143d4eb40412c","ref":"refs/heads/develop","pushedAt":"2024-05-05T20:38:49.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"tirix","name":null,"path":"/tirix","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5831830?s=80&v=4"},"commit":{"message":"Fix typo: definiton->definition (#3976)\n\nSigned-off-by: David A. Wheeler <dwheeler@dwheeler.com>","shortMessageHtmlLink":"Fix typo: definiton-&gt;definition (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2279716374\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3976\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3976/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3976\">#3976</a>)"}},{"before":null,"after":"a089eb1d252a9caba92a95e6845a76c11be2696d","ref":"refs/heads/definiton","pushedAt":"2024-05-05T20:31:46.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"david-a-wheeler","name":"David A. Wheeler","path":"/david-a-wheeler","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/813150?s=80&v=4"},"commit":{"message":"Fix typo: definiton->definition\n\nSigned-off-by: David A. Wheeler <dwheeler@dwheeler.com>","shortMessageHtmlLink":"Fix typo: definiton-&gt;definition"}},{"before":"4a29a60bbe76a33e1b36015855c1c9e988aa94cd","after":"040ac00ee62b706ea921bcf09db27c921f664158","ref":"refs/heads/develop","pushedAt":"2024-05-05T18:28:56.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"wlammen","name":"Wolf Lammen","path":"/wlammen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30736367?s=80&v=4"},"commit":{"message":"mathbox: add wl-cadan (#3972)\n\n* add wl-cadan\r\n\r\n* rm outdated OLD theorems\r\n\r\n* Revision by SN\r\n\r\n* discouraged\r\n\r\n* fix revision comment\r\n\r\n* rm more OLD theorems\r\n\r\n* discouraged\r\n\r\n* rm extra empty line","shortMessageHtmlLink":"mathbox: add wl-cadan (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2279172875\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3972\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3972/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3972\">#3972</a>)"}},{"before":"4a42e54dac8da96eff06da12327c8dd010b755e4","after":"4a29a60bbe76a33e1b36015855c1c9e988aa94cd","ref":"refs/heads/develop","pushedAt":"2024-05-04T14:48:19.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"wlammen","name":"Wolf Lammen","path":"/wlammen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30736367?s=80&v=4"},"commit":{"message":"alternative definition of cad (#3970)\n\n* alternative definition of cad\r\n\r\n* add wl-cad0/1\r\n\r\n* fix wording in wl-df-had","shortMessageHtmlLink":"alternative definition of cad (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2276107140\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3970\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3970/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3970\">#3970</a>)"}},{"before":"e0009afbd3429c7aa31e4c5fd8154cba2bcc2391","after":"4a42e54dac8da96eff06da12327c8dd010b755e4","ref":"refs/heads/develop","pushedAt":"2024-05-02T19:48:19.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"tirix","name":null,"path":"/tirix","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5831830?s=80&v=4"},"commit":{"message":"Two more countable choice consequences in iset.mm (#3969)\n\n* Add cc3 to iset.mm\r\n\r\nThis is axcc3 from set.mm except:\r\n\r\n* change non-empty to inhabited\r\n\r\n* put in deduction form especially the N ~~ _om and F e. _V hypotheses\r\n  (and in the case of the latter only require it to be supplied for\r\n  n e. N not any n )\r\n\r\n* F(n) must be inhabited at every n e. N not just where we want the\r\n  choice function to be defined.\r\n\r\n* countable choice is a hypothesis rather than an axiom.\r\n\r\nThe proof is loosely based on the axcc3 proof but is different in quite\r\na few details.\r\n\r\n* Add cc4 to iset.mm\r\n\r\nThis is axcc4 from set.mm with changes similar to the differences\r\nbetween axcc3 and cc3 .","shortMessageHtmlLink":"Two more countable choice consequences in iset.mm (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2274572353\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3969\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3969/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3969\">#3969</a>)"}},{"before":"a5c697610b0a51daba6320844f92ade3bbadcb4b","after":"e0009afbd3429c7aa31e4c5fd8154cba2bcc2391","ref":"refs/heads/develop","pushedAt":"2024-05-02T19:22:12.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"benjub","name":"Benoit","path":"/benjub","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/41090811?s=80&v=4"},"commit":{"message":"Mathbox: clarify proof of eliminablity. (#3968)","shortMessageHtmlLink":"Mathbox: clarify proof of eliminablity. (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2274366640\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3968\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3968/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3968\">#3968</a>)"}},{"before":"9238920e0f80bc23499298de6cf152887591a11e","after":"a5c697610b0a51daba6320844f92ade3bbadcb4b","ref":"refs/heads/develop","pushedAt":"2024-05-02T01:10:14.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"wlammen","name":"Wolf Lammen","path":"/wlammen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30736367?s=80&v=4"},"commit":{"message":"mathbox: wl-df-had update (#3967)\n\n* add wl-hadnot1\r\n\r\n* wl-df-had update\r\n\r\n* fix typos","shortMessageHtmlLink":"mathbox: wl-df-had update (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2273629434\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3967\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3967/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3967\">#3967</a>)"}},{"before":"cae908903cba767532bf744b7013ec3b72683506","after":"9238920e0f80bc23499298de6cf152887591a11e","ref":"refs/heads/develop","pushedAt":"2024-05-02T01:09:38.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"wlammen","name":"Wolf Lammen","path":"/wlammen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30736367?s=80&v=4"},"commit":{"message":"Reduction of ax-13 usage (#3966)\n\n* Reduction of ax-13 usage\r\n\r\nDependency on ax-13 removed from:\r\n\r\n* REAL AND COMPLEX NUMBERS: 2 theorems (~brfi1indALT and ~nfsum: ~nfsum made OLD, and ~nfsumw renamed to ~nfsum)\r\n* GRAPH THEORY: 1 theorem (~frgrwopreglem5ALT)\r\n* AV's mathbox: ~cbvral2, ~cbvrex2\r\n\r\nOther changes in AV's mathbox:\r\n* ~dfich2ai , ~dfich2bi, ~dfich2OLD removed (are obsolete)\r\n* ~ichnfimlem1: still depends on ax-13 (depends on ~ nfsb4t), usage discouraged, used by ~ ichnfimlem3\r\n* ~ichnfimlem2: still depends on ax-13 ax-13 (depends on ~ drsb1), usage discouraged, used by ~ichnfimlem3\r\n* ~ichnfimlem3: still depends on ax-13, usage discouraged, used by ~ichnfim\r\nichnfim: still depends on ax-13, usage discouraged, used by ~ichnfb\r\nichnfb: still depends on ax-13, usage discouraged, not used\r\n\r\n* discouraged, rewrap\r\n\r\n* dependency of ~ichnfimlem3, ~ichnfim, ~ichnfb on ax-13 removed\r\n\r\nas proposed by Gino Giotto.\r\n\r\nTypo detected by W. Lammen fixed.\r\n\r\n* reason for the revision","shortMessageHtmlLink":"Reduction of ax-13 usage (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2273295376\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3966\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3966/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3966\">#3966</a>)"}},{"before":"b32a182d43521326a8f1b5ef60eea7074a27fb15","after":"cae908903cba767532bf744b7013ec3b72683506","ref":"refs/heads/develop","pushedAt":"2024-04-30T18:43:13.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"wlammen","name":"Wolf Lammen","path":"/wlammen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30736367?s=80&v=4"},"commit":{"message":"Equation 1 and 2 of lcm inequality lemma (#3964)\n\n* Add first two equalities in lcm inequality lemma\r\n\r\n* Move itgpowd to mathbox\r\n\r\n* Move unitsscn from mathbox to main\r\n\r\n* Move elunitrn,elunitcn to main\r\n\r\n* Fixed typos\r\n\r\n* Add lcmineqlem3, that uses itgpowd","shortMessageHtmlLink":"Equation 1 and 2 of lcm inequality lemma (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2269533122\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3964\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3964/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3964\">#3964</a>)"}},{"before":"5ec0b5965d6c5d5c87cdda3452d6c9ff54369cb8","after":"b32a182d43521326a8f1b5ef60eea7074a27fb15","ref":"refs/heads/develop","pushedAt":"2024-04-30T08:50:56.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"wlammen","name":"Wolf Lammen","path":"/wlammen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30736367?s=80&v=4"},"commit":{"message":"shorten ifpdfbi (#3965)\n\n* shorten ifpdfbi\r\n\r\n* discouraged","shortMessageHtmlLink":"shorten ifpdfbi (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2270381615\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3965\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3965/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3965\">#3965</a>)"}},{"before":"457d0dec3b1689d8dfe10b2c68ea0a03c4ab181a","after":"5ec0b5965d6c5d5c87cdda3452d6c9ff54369cb8","ref":"refs/heads/develop","pushedAt":"2024-04-30T02:02:05.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"wlammen","name":"Wolf Lammen","path":"/wlammen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30736367?s=80&v=4"},"commit":{"message":"update wl-df-had (#3962)\n\n* update wl-df-had\r\n\r\n* fix missing proof\r\n\r\n* rename wl-hadbi -> wl-dfhad3\r\n\r\n* typo","shortMessageHtmlLink":"update wl-df-had (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2268121439\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3962\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3962/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3962\">#3962</a>)"}},{"before":"022734bd0eb8af1925b9c00e5b534dcb9afea029","after":"457d0dec3b1689d8dfe10b2c68ea0a03c4ab181a","ref":"refs/heads/develop","pushedAt":"2024-04-29T15:50:50.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"wlammen","name":"Wolf Lammen","path":"/wlammen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30736367?s=80&v=4"},"commit":{"message":"fix an error noted in #3931 (#3963)","shortMessageHtmlLink":"fix an error noted in <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2249582216\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3931\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3931/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3931\">#3931</a> (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2268770037\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3963\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3963/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3963\">#3963</a>)"}},{"before":"7a2b30bb955d16117928a5303ee760c165ade317","after":"022734bd0eb8af1925b9c00e5b534dcb9afea029","ref":"refs/heads/develop","pushedAt":"2024-04-29T15:33:19.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"jkingdon","name":"Jim Kingdon","path":"/jkingdon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16878?s=80&v=4"},"commit":{"message":"Add cc2 to iset.mm\n\nThis is axcc2 from set.mm except:\n\n* Change non-empty to inhabited\n\n* The sequence must be a function on _om and have an inhabited value at every\n  index in _om , not just those where we want the choice function to be defined.\n\n* add CCHOICE as a hypothesis\n\nIncludes lemma cc2lem which is similar to axcc2lem from set.mm.\n\nThe proof is generally based on the set.mm proof but different in a\nvariety of details.","shortMessageHtmlLink":"Add cc2 to iset.mm"}},{"before":"8f0bbdb7578660b9e9dd806b5755105a206094cf","after":"7a2b30bb955d16117928a5303ee760c165ade317","ref":"refs/heads/develop","pushedAt":"2024-04-29T07:02:28.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"tirix","name":null,"path":"/tirix","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5831830?s=80&v=4"},"commit":{"message":"First lemma in lcm inequality proof (#3959)\n\n* Add first equation sublemma in lcm inequality proof\r\n\r\n* fgh = gfh in gcd ineq lemma\r\n\r\n* Pull factor out integral aks first eq\r\n\r\n* move factor out of sum\r\n\r\n* First equality proven as chain of 4 equalities lcm inequality proof\r\n\r\n* Move bddiblnc, cnicciblnc from BL's mathbox to main set.mm\r\n\r\n* Remove 2 hypotheses from 3factsumint\r\n\r\n* Add additional documentation for proof\r\n\r\n* Add missing tilde","shortMessageHtmlLink":"First lemma in lcm inequality proof (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2266113948\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3959\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3959/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3959\">#3959</a>)"}},{"before":"5fc47a76eb570bc50660b119e01e42314c05a699","after":"8f0bbdb7578660b9e9dd806b5755105a206094cf","ref":"refs/heads/develop","pushedAt":"2024-04-28T10:37:30.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"tirix","name":null,"path":"/tirix","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5831830?s=80&v=4"},"commit":{"message":"Revision of hypotheses with an \"is a set\" property using the universal class _V (#3958)\n\n* Replace _V in hypotheses (1)\r\n\r\n for ~wlkp1 (and lemmas), ~eupthp1 and ~eupth2eucrct\r\n\r\n* Replace _V in hypotheses (2)\r\n\r\nfor ~isxmetd and ~isxmet2d\r\n\r\n* Replace _V in hypotheses (3)\r\n\r\nfor ~isfild (and ~isfildlem),\r\nused in ~snfil, ~fgcl, ~filuni, ~cfinfil, ~csdfil, ~supfil, ~fin1aufil\r\n\r\n* Replace _V in hypotheses (4): for ~ellspd\r\n\r\nused in ~elfilspd, ~islindf4, ~ellspds, ~fedgmul\r\n\r\n* Replace _V in hypotheses (5): for ~evlseu (and lemmas)\r\n\r\nand for ~psrbagev1 and ~psrbagev2.\r\n\r\nUsed in ~evlsval2.\r\n\r\n* Replace _V in hypotheses (6): for ~mplind\r\n\r\nUsed in ~mpfind.\r\n\r\n* Replace _V in hypotheses (7): for ~frgpnabllem1 /2, ~lsppropd, ~lbspropd\r\n\r\n- used in ~frgpnabll\r\n- used in ~lidlrsppropd, ~lindfpropd, ~lbspropd\r\n- used in ~dimpropd\r\n\r\n* Replace _V in hypotheses ((8): for ~lsmpropd\r\n\r\nUsed in ~hlhillsm\r\n\r\n* Replace _V in hypotheses (9): for ~isposd\r\n\r\nUsed in ~pospo, ~odupos, ~ipopos, ~zntoslem","shortMessageHtmlLink":"Revision of hypotheses with an \"is a set\" property using the universa…"}},{"before":"547daee3fc11ff375477f364e403549a44760e20","after":"5fc47a76eb570bc50660b119e01e42314c05a699","ref":"refs/heads/develop","pushedAt":"2024-04-28T10:07:17.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"tirix","name":null,"path":"/tirix","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5831830?s=80&v=4"},"commit":{"message":"Galois Connections (#3957)\n\n* Galois Connections\r\n\r\n* Merge remote-tracking branch 'upstream/develop' into galconn\r\n\r\n* Fix definition check\r\n\r\n* As per @savask comments\r\n\r\n* As per @avekens comments","shortMessageHtmlLink":"Galois Connections (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2265280293\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3957\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3957/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3957\">#3957</a>)"}},{"before":"e6191ff16485701497033860f01fd9d61d89d4d3","after":"547daee3fc11ff375477f364e403549a44760e20","ref":"refs/heads/develop","pushedAt":"2024-04-28T10:06:25.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"tirix","name":null,"path":"/tirix","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5831830?s=80&v=4"},"commit":{"message":"Update discussion of ruc in mmcomplex.html (#3931)\n\nThe current text has diverged quite a bit from the proof in set.mm (for\r\nexample, it refers to 39 lemmas, but set.mm has 13).  Update it to\r\nreflect the way the set.mm proof now works, but keep the overall\r\nstructure, and most of the text, intact.\r\n\r\nRefer to theorems (including lemmas) by using the ~ syntax which should\r\nreduce the chance of this happening again if the set.mm proof is changed\r\nagain to this extent.","shortMessageHtmlLink":"Update discussion of ruc in mmcomplex.html (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2249582216\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3931\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3931/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3931\">#3931</a>)"}},{"before":"92a0773c6929170fa2a981706680be8d37a398be","after":"e6191ff16485701497033860f01fd9d61d89d4d3","ref":"refs/heads/develop","pushedAt":"2024-04-28T07:46:19.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"tirix","name":null,"path":"/tirix","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5831830?s=80&v=4"},"commit":{"message":"Fix readme link (#3960)","shortMessageHtmlLink":"Fix readme link (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2267343219\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3960\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3960/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3960\">#3960</a>)"}},{"before":"73824f503fb2c70d33daf5797722afbfc8d12cc0","after":"92a0773c6929170fa2a981706680be8d37a398be","ref":"refs/heads/develop","pushedAt":"2024-04-26T09:21:16.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"tirix","name":null,"path":"/tirix","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5831830?s=80&v=4"},"commit":{"message":"Add inference lemmas for natural numbers (#3956)\n\n* Add inference lemmas for natural numbers\r\n\r\n* Laws for multiplication, inference natural numbers\r\n\r\n* Add inference version of gcdmultiple\r\n\r\n* Calculate gcd of 420 and 8\r\n\r\n* Add gcd of 12 and 5\r\n\r\n* Add gcd of 60 and 6\r\n\r\n* Add gcd of 60 and 7\r\n\r\n* Calculate lcm\r\n\r\n* add lcm results for lcm inequality lemma, base case\r\n\r\n* Add lemma to calculate lcm\r\n\r\n* Lcm of union of integers up to 3\r\n\r\n* Add remaining lcm union cases for base case","shortMessageHtmlLink":"Add inference lemmas for natural numbers (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2262986319\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3956\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3956/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3956\">#3956</a>)"}},{"before":"2e2a0324cb1108d0b9298788bdfebed28d72d015","after":"73824f503fb2c70d33daf5797722afbfc8d12cc0","ref":"refs/heads/develop","pushedAt":"2024-04-25T21:47:31.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"benjub","name":"Benoit","path":"/benjub","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/41090811?s=80&v=4"},"commit":{"message":"Mathbox: around bj-denotes. (#3952)","shortMessageHtmlLink":"Mathbox: around bj-denotes. (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2259893818\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3952\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3952/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3952\">#3952</a>)"}},{"before":"38651e3466a623ee59a311d98f1f9273241b5cf0","after":"2e2a0324cb1108d0b9298788bdfebed28d72d015","ref":"refs/heads/develop","pushedAt":"2024-04-25T08:53:25.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"wlammen","name":"Wolf Lammen","path":"/wlammen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30736367?s=80&v=4"},"commit":{"message":"alternative definition of had (#3953)\n\n* alternative definition of had\r\n\r\n* discouraged\r\n\r\n* rewrap\r\n\r\n* shorten wl-hadbi123d","shortMessageHtmlLink":"alternative definition of had (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2261631951\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3953\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3953/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3953\">#3953</a>)"}},{"before":"1a29a5660e5a2149aae0dba23278cb8181a1380e","after":null,"ref":"refs/heads/conventions_p","pushedAt":"2024-04-24T08:21:26.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"tirix","name":null,"path":"/tirix","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5831830?s=80&v=4"}},{"before":"ee95eeb613de05cb8f0b36e6fd511a8854d2cfda","after":"38651e3466a623ee59a311d98f1f9273241b5cf0","ref":"refs/heads/develop","pushedAt":"2024-04-24T08:21:25.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"tirix","name":null,"path":"/tirix","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5831830?s=80&v=4"},"commit":{"message":"tweak paragraph breaks in ~conventions (#3948)","shortMessageHtmlLink":"tweak paragraph breaks in ~conventions (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2257476857\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3948\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3948/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3948\">#3948</a>)"}},{"before":"8f76bf5e07eb8d6c343c87897e1d10fb648fc3f8","after":"ee95eeb613de05cb8f0b36e6fd511a8854d2cfda","ref":"refs/heads/develop","pushedAt":"2024-04-24T08:16:43.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"tirix","name":null,"path":"/tirix","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5831830?s=80&v=4"},"commit":{"message":"No double blank lines within sections. (#3951)","shortMessageHtmlLink":"No double blank lines within sections. (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2259667396\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3951\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3951/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3951\">#3951</a>)"}},{"before":"8b138f1cd3060980e100d3e91c709c7223b26af3","after":"8f76bf5e07eb8d6c343c87897e1d10fb648fc3f8","ref":"refs/heads/develop","pushedAt":"2024-04-23T23:50:30.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"wlammen","name":"Wolf Lammen","path":"/wlammen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30736367?s=80&v=4"},"commit":{"message":"Remove duplicate lemma itgeq2d (#3950)","shortMessageHtmlLink":"Remove duplicate lemma itgeq2d (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2259570230\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3950\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3950/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3950\">#3950</a>)"}},{"before":"d859be504748a01bfdbd9ebd01047d6c37b2cf13","after":"8b138f1cd3060980e100d3e91c709c7223b26af3","ref":"refs/heads/develop","pushedAt":"2024-04-23T20:20:35.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"jkingdon","name":"Jim Kingdon","path":"/jkingdon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16878?s=80&v=4"},"commit":{"message":"Add comments to *.raw.html files\n\nAdd a comment to clarify the process of turning the .raw.html file\nto an .html file. Seems useful to have the comment in both the .raw.html\ninput file and the generated .html file.","shortMessageHtmlLink":"Add comments to *.raw.html files"}},{"before":"1b49049d565c750686f859a8d12d105bd0e7796b","after":"d859be504748a01bfdbd9ebd01047d6c37b2cf13","ref":"refs/heads/develop","pushedAt":"2024-04-23T19:53:38.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"benjub","name":"Benoit","path":"/benjub","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/41090811?s=80&v=4"},"commit":{"message":"shorten norcom (#3949)\n\n* shorten norcom\r\n\r\n* fix comment of hadcoma\r\n\r\n* fix comment of xorbi12i\r\n\r\n* fix comment of rexcomOLD\r\n\r\n* fix comment of rnmptcOLD\r\n\r\n* fix comment of o2p2e4OLD\r\n\r\n* fix comment of ascldimulOLD\r\n\r\n* fix comment of wwlksnfiOLD","shortMessageHtmlLink":"shorten norcom (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2259274325\" data-permission-text=\"Title is private\" data-url=\"https://github.com/metamath/set.mm/issues/3949\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/metamath/set.mm/pull/3949/hovercard\" href=\"https://github.com/metamath/set.mm/pull/3949\">#3949</a>)"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEQnMonAA","startCursor":null,"endCursor":null}},"title":"Activity · metamath/set.mm"}