Ring Theory in Mizar (a Rosetta stone)
Alex Nelson thmprover _AT_ gmail.com <[email protected]> Sun, 28 Dec 2025 19:07:03 -0800
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <CAA+9CX2C1E_uuYhJs3izim6jWwd12219fd5Ws2+o1rTog1Grkw@mail.gmail.com> |
--0000000000002e272606470e8a64 Content-Type: text/plain; charset="UTF-8" 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 --0000000000002e272606470e8a64 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"ltr">Hello,<br><br>I have assembled a "Rosetta Stone"= summarizing results in Ring theory formalized in Mizar's MML:=C2=A0<a = href=3D"https://pqnelson.github.io/org-notes/comp-sci/theorem-provers/mizar= /rings.html">https://pqnelson.github.io/org-notes/comp-sci/theorem-provers/= mizar/rings.html</a><div><br></div><div>I used Dummit and Foote's=C2=A0= "Abstract Algebra" (chapters 7 through the first half of chapter = 9) as the reference text, since this is what Caltech's Math 5B course t= eaches for ring theory.<br><br>Doubtless I have missed something, which is = an oversight/failing on my part, so if I accidentally marked a result as &q= uot;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 gap= s", so if you want to submit to the MML something which is missing, fe= el free!)<br><br>I intend to do another Rosetta stone for fields and Galois= theory, hopefully before next week.<br><br>Happy new year=C2=A0to everyone= , I hope everyone is happy and healthy and well.<br><br>Best,<br>Alex</div>= </div> --0000000000002e272606470e8a64--