# Homotopy Type Theory ring > history (Rev #11)

## Definition

A ring is an abelian group $R$ with an element $1:R$ and a abelian group homomorphism $\alpha:R \to (R \times R)$ such that

• $\alpha(1) = \mathrm{id}_R$

• for all $a:R$, $\alpha(a)(1) = a$

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

We define the bilinear function $(-)\cdot(-):M \times M \to M$ as

$a \cdot b \coloneqq \alpha(a)(b)$