{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":775900558,"defaultBranch":"master","name":"flt3","ownerLogin":"riccardobrasca","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2024-03-22T09:16:44.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/32490532?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1715002854.0","currentOid":""},"activityList":{"items":[{"before":"945d0aed2deb1057cd91930e614c2f404d1c25ef","after":"e7f8239dc11ee1734bdc597131d76fb780bcf3ba","ref":"refs/heads/master","pushedAt":"2024-06-25T11:01:30.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"},"commit":{"message":"bump","shortMessageHtmlLink":"bump"}},{"before":"6dd0a35b8c5af39113b355ac365ef5682b0717a4","after":"945d0aed2deb1057cd91930e614c2f404d1c25ef","ref":"refs/heads/master","pushedAt":"2024-06-25T09:13:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"},"commit":{"message":"bump","shortMessageHtmlLink":"bump"}},{"before":"27bd17eaa32dfa3d2b5b369dadd06504d7a0120b","after":"6dd0a35b8c5af39113b355ac365ef5682b0717a4","ref":"refs/heads/master","pushedAt":"2024-06-13T14:11:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"},"commit":{"message":"nicer","shortMessageHtmlLink":"nicer"}},{"before":"f04b9c867c7c37cbe7525d1253b46fd2e70fb982","after":"27bd17eaa32dfa3d2b5b369dadd06504d7a0120b","ref":"refs/heads/master","pushedAt":"2024-06-11T16:08:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"},"commit":{"message":"fix this","shortMessageHtmlLink":"fix this"}},{"before":"b7fb658ec06ae1b43adc98b723406d05f34578d1","after":"f04b9c867c7c37cbe7525d1253b46fd2e70fb982","ref":"refs/heads/master","pushedAt":"2024-06-11T15:52:13.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"},"commit":{"message":"bump","shortMessageHtmlLink":"bump"}},{"before":"d950adcb1585c0c05d1b22631a1b39ac44a0bccd","after":"b7fb658ec06ae1b43adc98b723406d05f34578d1","ref":"refs/heads/master","pushedAt":"2024-05-23T12:59:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"},"commit":{"message":"bump","shortMessageHtmlLink":"bump"}},{"before":"48a4da7423b491d5edb10f949bc7bfc6dbb35797","after":"d950adcb1585c0c05d1b22631a1b39ac44a0bccd","ref":"refs/heads/master","pushedAt":"2024-05-17T10:12:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"},"commit":{"message":"golf","shortMessageHtmlLink":"golf"}},{"before":"f78b1bfb0d86a617f4342f216d82358058b690e1","after":"48a4da7423b491d5edb10f949bc7bfc6dbb35797","ref":"refs/heads/master","pushedAt":"2024-05-17T10:01:11.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"},"commit":{"message":"useless","shortMessageHtmlLink":"useless"}},{"before":"768a134c8bd7d30fd7cdc7c04e3c5d3df4a6e968","after":"f78b1bfb0d86a617f4342f216d82358058b690e1","ref":"refs/heads/master","pushedAt":"2024-05-16T09:24:14.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"},"commit":{"message":"bump","shortMessageHtmlLink":"bump"}},{"before":"9a6571a49a3b045ca040daf311f3dda03ce371d4","after":"768a134c8bd7d30fd7cdc7c04e3c5d3df4a6e968","ref":"refs/heads/master","pushedAt":"2024-05-08T12:25:44.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"},"commit":{"message":"bump","shortMessageHtmlLink":"bump"}},{"before":"05f37e7a01486086b31b427b05c354ac665a32d7","after":"9a6571a49a3b045ca040daf311f3dda03ce371d4","ref":"refs/heads/master","pushedAt":"2024-05-06T13:54:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"},"commit":{"message":"bump","shortMessageHtmlLink":"bump"}},{"before":"2e254032ae4d39769d7effd4b96c5342043727a4","after":null,"ref":"refs/heads/faster","pushedAt":"2024-05-06T13:40:54.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"}},{"before":"fcea2763b86ef4b58c685880cfb902f6801e3b4c","after":"05f37e7a01486086b31b427b05c354ac665a32d7","ref":"refs/heads/master","pushedAt":"2024-04-23T08:59:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"},"commit":{"message":"faster?","shortMessageHtmlLink":"faster?"}},{"before":"2198c5b430712b433ffd446cc64b63f44879c5a8","after":"fcea2763b86ef4b58c685880cfb902f6801e3b4c","ref":"refs/heads/master","pushedAt":"2024-04-19T23:09:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"Simplify proof of `final`","shortMessageHtmlLink":"Simplify proof of <code>final</code>"}},{"before":"b00b1da0d10e60b7574c3abec2b4c80aa90df80f","after":"2198c5b430712b433ffd446cc64b63f44879c5a8","ref":"refs/heads/master","pushedAt":"2024-04-19T23:06:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"Simplify proof of `final`","shortMessageHtmlLink":"Simplify proof of <code>final</code>"}},{"before":"7ea95535778e12f68d36fadf03b374c2523eb65a","after":"b00b1da0d10e60b7574c3abec2b4c80aa90df80f","ref":"refs/heads/master","pushedAt":"2024-04-18T22:55:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"Simplify proof of `associated_of_dvd_a_add_b_of_dvd_a_add_eta_sq_mul_b`","shortMessageHtmlLink":"Simplify proof of <code>associated_of_dvd_a_add_b_of_dvd_a_add_eta_sq_mul_b</code>"}},{"before":"2b98c497f67640b1e66c74065b546d1f55887762","after":"7ea95535778e12f68d36fadf03b374c2523eb65a","ref":"refs/heads/master","pushedAt":"2024-04-17T12:46:26.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"},"commit":{"message":"bump","shortMessageHtmlLink":"bump"}},{"before":"9eb081fede726f779a3c0ce8405e2c0bd4b8a76e","after":"2b98c497f67640b1e66c74065b546d1f55887762","ref":"refs/heads/master","pushedAt":"2024-04-17T08:45:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"},"commit":{"message":"this is better","shortMessageHtmlLink":"this is better"}},{"before":"56d0aa074921793a178b11f4c057032de574403b","after":"9eb081fede726f779a3c0ce8405e2c0bd4b8a76e","ref":"refs/heads/master","pushedAt":"2024-04-17T08:35:38.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"},"commit":{"message":"bump","shortMessageHtmlLink":"bump"}},{"before":"a25b9e999b9dc0fac30f8b6a9b24ea06b5d405ce","after":"56d0aa074921793a178b11f4c057032de574403b","ref":"refs/heads/master","pushedAt":"2024-04-16T21:05:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"Improve proof of `lambda_sq_dvd_or_dvd_or_dvd`","shortMessageHtmlLink":"Improve proof of <code>lambda_sq_dvd_or_dvd_or_dvd</code>"}},{"before":"5e8a31f6585208915fb0ed7221b41a68d0305b52","after":"a25b9e999b9dc0fac30f8b6a9b24ea06b5d405ce","ref":"refs/heads/master","pushedAt":"2024-04-16T14:18:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"Fix docstring of theorem `Units.mem`","shortMessageHtmlLink":"Fix docstring of theorem <code>Units.mem</code>"}},{"before":"bdd761869bbcb1f3e53877b2f0017df56d4c1195","after":"5e8a31f6585208915fb0ed7221b41a68d0305b52","ref":"refs/heads/master","pushedAt":"2024-04-16T08:47:57.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"riccardobrasca","name":"Riccardo Brasca","path":"/riccardobrasca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32490532?s=80&v=4"},"commit":{"message":"bump","shortMessageHtmlLink":"bump"}},{"before":"77279dab3b2d46e136f27dba334112fea17c65d3","after":"bdd761869bbcb1f3e53877b2f0017df56d4c1195","ref":"refs/heads/master","pushedAt":"2024-04-15T22:34:31.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"Refactor `formula2`","shortMessageHtmlLink":"Refactor <code>formula2</code>"}},{"before":"e753867f6e66f8b38b0893dbe1beb7530d014939","after":"77279dab3b2d46e136f27dba334112fea17c65d3","ref":"refs/heads/master","pushedAt":"2024-04-11T09:20:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"Update FLT3.lean","shortMessageHtmlLink":"Update FLT3.lean"}},{"before":"d67a5cc739f815f4a3ae4397453fa71fb10bd030","after":"e753867f6e66f8b38b0893dbe1beb7530d014939","ref":"refs/heads/master","pushedAt":"2024-04-11T09:07:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"Remove Ideal namespace","shortMessageHtmlLink":"Remove Ideal namespace"}},{"before":"d2d37112628f925e1e891a9e7d5d3a53b1e16b79","after":"d67a5cc739f815f4a3ae4397453fa71fb10bd030","ref":"refs/heads/master","pushedAt":"2024-04-11T09:04:00.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"Remove useless lemma (`span_x_mul_span_y_mul_span_z`)","shortMessageHtmlLink":"Remove useless lemma (<code>span_x_mul_span_y_mul_span_z</code>)"}},{"before":"84a5e286bd77f806bf474e85e84919b384e1abc9","after":"d2d37112628f925e1e891a9e7d5d3a53b1e16b79","ref":"refs/heads/master","pushedAt":"2024-04-10T23:01:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"Add `lambda_ne_zero` in Cyclo.lean","shortMessageHtmlLink":"Add <code>lambda_ne_zero</code> in Cyclo.lean"}},{"before":"1e1437a64c94bd61de07f78c0feca06665347a7d","after":"84a5e286bd77f806bf474e85e84919b384e1abc9","ref":"refs/heads/master","pushedAt":"2024-04-10T23:00:36.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"Move `lambda_ne_zero` to Cyclo.lean","shortMessageHtmlLink":"Move <code>lambda_ne_zero</code> to Cyclo.lean"}},{"before":"a4d976c64bef4d995eea827995cea77eb2483d99","after":"1e1437a64c94bd61de07f78c0feca06665347a7d","ref":"refs/heads/master","pushedAt":"2024-04-10T22:57:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"Update docstring in FLT3.lean","shortMessageHtmlLink":"Update docstring in FLT3.lean"}},{"before":"78a18a3c9bed7ba58b9a09415d87794093a4b73e","after":"a4d976c64bef4d995eea827995cea77eb2483d99","ref":"refs/heads/master","pushedAt":"2024-04-09T23:27:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"Fix docstring","shortMessageHtmlLink":"Fix docstring"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEboIzSAA","startCursor":null,"endCursor":null}},"title":"Activity · riccardobrasca/flt3"}