the bottom of the PR list

Stream: general

[Johan Commelin]

@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]

That is so cool :-)

[Patrick Massot]

Thanks go to Kenny too!

[Kevin Buzzard]

for putting it there in the first place :-)

[Aniruddh Agarwal]

@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]

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