Zulip Chat Archive

Stream: general

Topic: the bottom of the PR list


view this post on Zulip Johan Commelin (May 16 2020 at 18:02):

@Aniruddh Agarwal adopted the PR on the bottom of the PR list, and now it's on the merge queue! Jacobson radical is coming to mathlib :octopus:

view this post on Zulip Kevin Buzzard (May 16 2020 at 18:02):

That is so cool :-)

view this post on Zulip Patrick Massot (May 16 2020 at 18:03):

Thanks go to Kenny too!

view this post on Zulip Kevin Buzzard (May 16 2020 at 18:07):

for putting it there in the first place :-)

view this post on Zulip Aniruddh Agarwal (May 16 2020 at 22:59):

@Johan Commelin @Bryan Gin-ge Chen The PR had an error, but that's fixed now and the CI is passing, so it should be OK to merge

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 00:07):

@Aniruddh Agarwal It's back on the queue. Thanks!


Last updated: May 14 2021 at 07:19 UTC