mathlib documentation


The forgetful functor from ℤ-modules to additive commutative groups is an equivalence of categories.

TODO: either use this equivalence to transport the monoidal structure from Module to Ab, or, having constructed that monoidal structure directly, show this functor is monoidal.


The forgetful functor from modules to AddCommGroup is full.