# Homotopy Type Theory commutative discrete reciprocal ring > history (Rev #1)

## Definition

A discrete reciprocal ring is a ring $(A, +, -, 0, \cdot, 1)$ with a commutative identity for $\cdot$:

$m_\kappa:\prod_{(a:A)} \prod_{(b:A)} a\cdot b = b\cdot a$

## Properties

Every commutative discrete reciprocal ring is a commutative discrete division ring.