This chapter describes the module system. Its purpose is to allow reusing of theory. For instance you can define the notion of groups and prove some of their properties. Then, you can define fields and reuse your group module twice (for multiplication and addition).