Hello,
I have assembled a "Rosetta Stone" summarizing results in Ring theory formalized in Mizar's MML:
https://pqnelson.github.io/org-notes/comp-sci/theorem-provers/mizar/rings.html
I used Dummit and Foote's "Abstract Algebra" (chapters 7 through the first half of chapter 9) as the reference text, since this is what Caltech's Math 5B course teaches for ring theory.
Doubtless I have missed something, which is an oversight/failing on my part, so if I accidentally marked a result as "missing from Mizar" but it's really in the MML, please let me know and I will update it. (I have no intention of "filling in the gaps", so if you want to submit to the MML something which is missing, feel free!)
I intend to do another Rosetta stone for fields and Galois theory, hopefully before next week.
Happy new year to everyone, I hope everyone is happy and healthy and well.
Best,
Alex