Metamath Proof Explorer

Table of Contents - 21.41. Mathbox for Rohan Ridenour

1. Misc
   1. spALT
   2. rr-spce
   3. rexlimdvaacbv
   4. rexlimddvcbvw
   5. rexlimddvcbv
   6. rr-elrnmpt3d
   7. rr-phpd
   8. tfindsd
2. Monoid rings
   1. cmnring
   2. df-mnring
   3. mnringvald
   4. mnringnmulrd
   5. mnringbased
   6. mnringbaserd
   7. mnringelbased
   8. mnringbasefd
   9. mnringbasefsuppd
   10. mnringaddgd
   11. mnring0gd
   12. mnring0g2d
   13. mnringmulrd
   14. mnringscad
   15. mnringvscad
   16. mnringlmodd
   17. mnringmulrvald
   18. mnringmulrcld
3. Shorter primitive equivalent of ax-groth
   1. Grothendieck universes are closed under collection
   2. Minimal universes
   3. Primitive equivalent of ax-groth