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