## Definition ## A __ring__ is an abelian group $R$ with a term $1:R$, a [[bilinear function]] $(-)\cdot(-):R \times R \to R$, and a [[abelian group homomorphism]] $\alpha:R \to (R \times R)$ such that * $\alpha(1) = \mathrm{id}_R$ * for all $a:R$ and $b:R$, $\alpha(a) \circ \alpha(b) = \alpha(a \cdot b)$ ## Examples ## * Every [[contractible type]] is a ring. * The [[integers]] are a ring. * The [[rational numbers]] are a ring. ## See also ## * [[commutative ring]] * [[power function]] * [[polynomial function]]