# Homotopy Type Theory module > history (changes)

Showing changes from revision #6 to #7: Added | Removed | Changed

## Definiton

Let

$A$ be an abelian group, let $R$ be a commutative ring. $A$ is an $R$-module if it comes with an abelian group homomorphism $\alpha:R \to (A \to A)$ such that

• $\alpha(1) = id_A$

• for all $a:R$ and $b:R$, $\alpha(a) \circ \alpha(b) = \alpha(a \cdot b)$

## Properties

Every abelian group is a $\mathbb{Z}$-module.