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

## Definition

A commutative Heyting reciprocal ring is a Heyting reciprocal 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 Heyting reciprocal ring is a commutative Heyting division ring.

## See also

Revision on March 14, 2022 at 23:48:53 by Anonymous?. See the history of this page for a list of all contributions to it.