{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":365697493,"defaultBranch":"master","name":"mathlib4","ownerLogin":"leanprover-community","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2021-05-09T07:52:01.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/41703605?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1717200222.0","currentOid":""},"activityList":{"items":[{"before":"b761afb6efcec3ad2a08ea96125e514dfb642d62","after":"0f7d22cacb46a8c3465b6e4b5d5654e56dd53ec7","ref":"refs/heads/dupuisf/StarOrderedRing_OrderedSMul","pushedAt":"2024-06-01T00:25:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"dupuisf","name":"Frédéric Dupuis","path":"/dupuisf","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/31101893?s=80&v=4"},"commit":{"message":"disambiguation","shortMessageHtmlLink":"disambiguation"}},{"before":null,"after":"2e3041181d274ce7eb4fd1df8e123330675eb41a","ref":"refs/heads/tb_finite2","pushedAt":"2024-06-01T00:03:42.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"tb65536","name":"Thomas Browning","path":"/tb65536","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/13339017?s=80&v=4"},"commit":{"message":"Refactor Finite.lean","shortMessageHtmlLink":"Refactor Finite.lean"}},{"before":"e24b46235344aaa66808b9ea5e4af6b6b238b8d9","after":null,"ref":"refs/heads/staging.tmp","pushedAt":"2024-06-01T00:00:13.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mathlib-bors[bot]","name":null,"path":"/apps/mathlib-bors","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/421226?s=80&v=4"}},{"before":"c9c411cbec9b019a6d7303c2902f27787dd6ea70","after":"8200298551e8ab76477ab483e6ff90730cfd6aff","ref":"refs/heads/staging","pushedAt":"2024-06-01T00:00:13.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"mathlib-bors[bot]","name":null,"path":"/apps/mathlib-bors","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/421226?s=80&v=4"},"commit":{"message":"chore: move LinearOrder Nat instance to Mathlib.Data.Nat.Defs (#13082)","shortMessageHtmlLink":"chore: move LinearOrder Nat instance to Mathlib.Data.Nat.Defs (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2308151630\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/mathlib4/issues/13082\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/mathlib4/pull/13082/hovercard\" href=\"https://github.com/leanprover-community/mathlib4/pull/13082\">#13082</a>)"}},{"before":"baa113885a5b2ad5d46761c7294a9ff472de248e","after":null,"ref":"refs/heads/staging-squash-merge.tmp","pushedAt":"2024-06-01T00:00:12.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mathlib-bors[bot]","name":null,"path":"/apps/mathlib-bors","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/421226?s=80&v=4"}},{"before":"b2e694839faa4e32d16f71f6f361b61e806fc1c7","after":"baa113885a5b2ad5d46761c7294a9ff472de248e","ref":"refs/heads/staging-squash-merge.tmp","pushedAt":"2024-06-01T00:00:12.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"mathlib-bors[bot]","name":null,"path":"/apps/mathlib-bors","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/421226?s=80&v=4"},"commit":{"message":"[ci skip][skip ci][skip netlify] -bors-staging-tmp-933dd6e847599a3d19bc128291d1aec8f8ca7e8c","shortMessageHtmlLink":"[ci skip][skip ci][skip netlify] -bors-staging-tmp-933dd6e847599a3d19…"}},{"before":"daa801e2817b8d28ecaa9f0b363af8f8cde0cbc3","after":"b2e694839faa4e32d16f71f6f361b61e806fc1c7","ref":"refs/heads/staging-squash-merge.tmp","pushedAt":"2024-06-01T00:00:11.000Z","pushType":"push","commitsCount":79,"pusher":{"login":"mathlib-bors[bot]","name":null,"path":"/apps/mathlib-bors","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/421226?s=80&v=4"},"commit":{"message":"[ci skip][skip ci][skip netlify] -bors-staging-tmp-1e7fb563c723fa2e787bee3cbb4d5af4862267bb","shortMessageHtmlLink":"[ci skip][skip ci][skip netlify] -bors-staging-tmp-1e7fb563c723fa2e78…"}},{"before":null,"after":"daa801e2817b8d28ecaa9f0b363af8f8cde0cbc3","ref":"refs/heads/staging-squash-merge.tmp","pushedAt":"2024-06-01T00:00:10.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mathlib-bors[bot]","name":null,"path":"/apps/mathlib-bors","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/421226?s=80&v=4"},"commit":{"message":"chore: remove most of the material on BitVec (#13286)\n\nThis PR removes most of the material on BitVec. While it is being actively developed in Lean, we do not want conflicting, but essentially unused, material here causing conflicts.\r\n\r\nIf downstream users of Mathlib find that they need some of this material is being used, they are advised to either:\r\n* restore the material in their downstream repository\r\n* ask someone from the FRO, e.g. @semorrison, about making a PR adding it to the Lean library.\r\n\r\n\r\n\r\n\n\nCo-authored-by: Alex Keizer <alex@keizer.dev>\nCo-authored-by: Kim Morrison <kim@tqft.net>","shortMessageHtmlLink":"chore: remove most of the material on BitVec (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2319468060\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/mathlib4/issues/13286\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/mathlib4/pull/13286/hovercard\" href=\"https://github.com/leanprover-community/mathlib4/pull/13286\">#13286</a>)"}},{"before":"9c48b33e42f73b07484bba0c14caba33d0269797","after":"e24b46235344aaa66808b9ea5e4af6b6b238b8d9","ref":"refs/heads/staging.tmp","pushedAt":"2024-06-01T00:00:09.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"mathlib-bors[bot]","name":null,"path":"/apps/mathlib-bors","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/421226?s=80&v=4"},"commit":{"message":"[ci skip][skip ci][skip netlify] -bors-staging-tmp-13082","shortMessageHtmlLink":"[ci skip][skip ci][skip netlify] -bors-staging-tmp-13082"}},{"before":"2240d50631387984dbd7a9093a8ff1b2b703fa01","after":"9c48b33e42f73b07484bba0c14caba33d0269797","ref":"refs/heads/staging.tmp","pushedAt":"2024-06-01T00:00:09.000Z","pushType":"push","commitsCount":79,"pusher":{"login":"mathlib-bors[bot]","name":null,"path":"/apps/mathlib-bors","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/421226?s=80&v=4"},"commit":{"message":"[ci skip][skip ci][skip netlify] -bors-staging-tmp-12970","shortMessageHtmlLink":"[ci skip][skip ci][skip netlify] -bors-staging-tmp-12970"}},{"before":null,"after":"2240d50631387984dbd7a9093a8ff1b2b703fa01","ref":"refs/heads/staging.tmp","pushedAt":"2024-06-01T00:00:08.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mathlib-bors[bot]","name":null,"path":"/apps/mathlib-bors","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/421226?s=80&v=4"},"commit":{"message":"[ci skip][skip ci][skip netlify]","shortMessageHtmlLink":"[ci skip][skip ci][skip netlify]"}},{"before":"379e3b2a2b15c25f61a8883003d43a57d2fd8860","after":"0d762441b6b7346e4c6c2efbc96a00b2d840e221","ref":"refs/heads/lean-pr-testing-4319","pushedAt":"2024-05-31T23:33:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"leanprover-community-mathlib4-bot","name":null,"path":"/leanprover-community-mathlib4-bot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/129911861?s=80&v=4"},"commit":{"message":"Trigger CI for https://github.com/leanprover/lean4/pull/4319","shortMessageHtmlLink":"Trigger CI for <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2328651165\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/4319\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/4319/hovercard\" href=\"https://github.com/leanprover/lean4/pull/4319\">leanprover/lean4#4319</a>"}},{"before":null,"after":"ff0d652f99e638f1738e1957fd27d92296e44159","ref":"refs/heads/tb_finite1","pushedAt":"2024-05-31T23:26:12.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"tb65536","name":"Thomas Browning","path":"/tb65536","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/13339017?s=80&v=4"},"commit":{"message":"Refactor Coset.lean","shortMessageHtmlLink":"Refactor Coset.lean"}},{"before":"944f7df591dd05e7cca38169ce79a2f234769704","after":"7eb903cc20a786583bbda01af81bc9ed4d8c8948","ref":"refs/heads/dagur/CondensedEpi","pushedAt":"2024-05-31T23:24:50.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"dagurtomas","name":"Dagur Tómas Ásgeirsson","path":"/dagurtomas","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25623829?s=80&v=4"},"commit":{"message":"golf","shortMessageHtmlLink":"golf"}},{"before":"c58e8485efa25b473cb666ea781e5655fc368bf3","after":"944f7df591dd05e7cca38169ce79a2f234769704","ref":"refs/heads/dagur/CondensedEpi","pushedAt":"2024-05-31T23:20:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"dagurtomas","name":"Dagur Tómas Ásgeirsson","path":"/dagurtomas","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25623829?s=80&v=4"},"commit":{"message":"characterise epimorphisms in categories of condensed objects","shortMessageHtmlLink":"characterise epimorphisms in categories of condensed objects"}},{"before":"05c3fcfade38fea741b391dbd83b1f3c43915ad1","after":"2235ae5100e2af7f16bea313637531b24bf8e1e0","ref":"refs/heads/feat_namespace_mathlib_vector","pushedAt":"2024-05-31T23:20:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Shreyas4991","name":"Shrys","path":"/Shreyas4991","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4014341?s=80&v=4"},"commit":{"message":"Minimised namespace opening","shortMessageHtmlLink":"Minimised namespace opening"}},{"before":"a59c13fa8cc9180657f11d3438a090c7c4a905b8","after":"92ae2dc44e8d022492ccb838939b73a8bb8faea3","ref":"refs/heads/StevenClontz/regular-lindelof-2","pushedAt":"2024-05-31T23:17:43.000Z","pushType":"push","commitsCount":198,"pusher":{"login":"StevenClontz","name":"Steven Clontz","path":"/StevenClontz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1559632?s=80&v=4"},"commit":{"message":"Merge branch 'master' into StevenClontz/regular-lindelof-2","shortMessageHtmlLink":"Merge branch 'master' into StevenClontz/regular-lindelof-2"}},{"before":null,"after":"8c7e2497d6b5ded2cb20ad30538ebffa5560f7a2","ref":"refs/heads/tb_sylow_cleanup","pushedAt":"2024-05-31T23:09:31.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"tb65536","name":"Thomas Browning","path":"/tb65536","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/13339017?s=80&v=4"},"commit":{"message":"temp pass","shortMessageHtmlLink":"temp pass"}},{"before":"70e2f19638c4514e376cbb84810b1e69a0ff1a8e","after":"a59c13fa8cc9180657f11d3438a090c7c4a905b8","ref":"refs/heads/StevenClontz/regular-lindelof-2","pushedAt":"2024-05-31T23:08:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"StevenClontz","name":"Steven Clontz","path":"/StevenClontz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1559632?s=80&v=4"},"commit":{"message":"clean up simps","shortMessageHtmlLink":"clean up simps"}},{"before":"12822e9f944a56ce4cd57597742ac465b5773d8b","after":"70e2f19638c4514e376cbb84810b1e69a0ff1a8e","ref":"refs/heads/StevenClontz/regular-lindelof-2","pushedAt":"2024-05-31T23:06:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"StevenClontz","name":"Steven Clontz","path":"/StevenClontz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1559632?s=80&v=4"},"commit":{"message":"proved countable_covers_to_separated_nhds","shortMessageHtmlLink":"proved countable_covers_to_separated_nhds"}},{"before":null,"after":"86a7846b5bbe9a6434538c52c97517424f98e6ac","ref":"refs/heads/ScottCarnahan/Multichoose_neg","pushedAt":"2024-05-31T22:53:03.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ScottCarnahan","name":"Scott Carnahan","path":"/ScottCarnahan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/128885296?s=80&v=4"},"commit":{"message":"Multichoose at negative arguments","shortMessageHtmlLink":"Multichoose at negative arguments"}},{"before":"9813f4080133d2d54c7c8c7bff56c3d0a891f639","after":"9355b8655fb29c4f4891218e72ee04a3b6ef1e24","ref":"refs/heads/rida/cache","pushedAt":"2024-05-31T22:45:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Rida-Hamadani","name":"Rida Hamadani","path":"/Rida-Hamadani","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/106540880?s=80&v=4"},"commit":{"message":"remove `s!` macro\n\nCo-authored-by: grunweg <rothgami@math.hu-berlin.de>","shortMessageHtmlLink":"remove <code>s!</code> macro"}},{"before":null,"after":"379e3b2a2b15c25f61a8883003d43a57d2fd8860","ref":"refs/heads/lean-pr-testing-4319","pushedAt":"2024-05-31T22:31:49.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"leanprover-community-mathlib4-bot","name":null,"path":"/leanprover-community-mathlib4-bot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/129911861?s=80&v=4"},"commit":{"message":"Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/4319","shortMessageHtmlLink":"Update lean-toolchain for testing <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2328651165\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/4319\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/4319/hovercard\" href=\"https://github.com/leanprover/lean4/pull/4319\">leanprover/lean4#4319</a>"}},{"before":"ecb25a707c5020a1e9f40044be049c7524757e38","after":"cc6d998807e80e304826185fd093ef75b54b0a67","ref":"refs/heads/elementwise","pushedAt":"2024-05-31T22:31:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rmbellovin","name":"Rebecca Bellovin","path":"/rmbellovin","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/48215858?s=80&v=4"},"commit":{"message":"Update Mathlib/Lean/Meta/Simp.lean : linting\n\nCo-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>","shortMessageHtmlLink":"Update Mathlib/Lean/Meta/Simp.lean : linting"}},{"before":"6495e45ff0fff6680448406a8efa71c32656c8e6","after":"18a53a3789b4ca227fb924094f767a0b7d8eea05","ref":"refs/heads/EllipticCurve.Affine.Map","pushedAt":"2024-05-31T22:28:05.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Multramate","name":"David Kurniadi Angdinata","path":"/Multramate","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25112641?s=80&v=4"},"commit":{"message":"Rename variable","shortMessageHtmlLink":"Rename variable"}},{"before":"ed8ba8c8e0496f96ee21bb424d15932d2846e1ab","after":"ecb25a707c5020a1e9f40044be049c7524757e38","ref":"refs/heads/elementwise","pushedAt":"2024-05-31T22:27:49.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rmbellovin","name":"Rebecca Bellovin","path":"/rmbellovin","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/48215858?s=80&v=4"},"commit":{"message":"add line break to fix linter complaint","shortMessageHtmlLink":"add line break to fix linter complaint"}},{"before":"c937fa95ed930cfdb427ae28a813bb4066a1f9a8","after":"e2f09e600bfeac18c2bc18fa42b9b61854a54a3f","ref":"refs/heads/lean-pr-testing-4272","pushedAt":"2024-05-31T22:21:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"leanprover-community-mathlib4-bot","name":null,"path":"/leanprover-community-mathlib4-bot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/129911861?s=80&v=4"},"commit":{"message":"Trigger CI for https://github.com/leanprover/lean4/pull/4272","shortMessageHtmlLink":"Trigger CI for <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2316389562\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/4272\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/4272/hovercard\" href=\"https://github.com/leanprover/lean4/pull/4272\">leanprover/lean4#4272</a>"}},{"before":"da9c9c158a8d8e759f853a773e79f79972a57c25","after":"a5ea7e77875e3a4820cfd3afe9fd652395cc70b1","ref":"refs/heads/MR-rewrite-copyright-linter","pushedAt":"2024-05-31T22:06:34.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"grunweg","name":null,"path":"/grunweg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10105016?s=80&v=4"},"commit":{"message":"Move the Lean check to lint-style.sh instead.","shortMessageHtmlLink":"Move the Lean check to lint-style.sh instead."}},{"before":"b2c5eb9d19465f5c0af3dd21f0523b3ad848a1d0","after":"da9c9c158a8d8e759f853a773e79f79972a57c25","ref":"refs/heads/MR-rewrite-copyright-linter","pushedAt":"2024-05-31T22:03:55.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"grunweg","name":null,"path":"/grunweg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10105016?s=80&v=4"},"commit":{"message":"Move the Lean check to lint-style.sh instead.","shortMessageHtmlLink":"Move the Lean check to lint-style.sh instead."}},{"before":"79925ed463cb6df61e0f241b19a84679a393e2c5","after":"a3dfa510b7b510303da4bb80261fe50afbb2b761","ref":"refs/heads/MR-debug-nolint-workflow","pushedAt":"2024-05-31T21:51:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"grunweg","name":null,"path":"/grunweg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10105016?s=80&v=4"},"commit":{"message":"Inline script and remove all problem-matcher goop.","shortMessageHtmlLink":"Inline script and remove all problem-matcher goop."}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEWXuPUQA","startCursor":null,"endCursor":null}},"title":"Activity · leanprover-community/mathlib4"}