Zulip Chat Archive

Stream: general

Topic: the bottom of the PR list


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:

Kevin Buzzard (May 16 2020 at 18:02):

That is so cool :-)

Patrick Massot (May 16 2020 at 18:03):

Thanks go to Kenny too!

Kevin Buzzard (May 16 2020 at 18:07):

for putting it there in the first place :-)

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

Bryan Gin-ge Chen (May 17 2020 at 00:07):

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


Last updated: Aug 03 2023 at 10:10 UTC