Commutative Algebra in the Mizar System

摘要

We report on the development of algebra in the Mizar system. This includes the construc- tion of formal multivariate power series and polynomials as well as the definition of ideals up to a proof of the Hilbert basis theorem. We present how the algebraic structures are handled and how we inherited the past developments from the Miar Mathematical Li- brary (MML).