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

Definition

A commutative Heyting cancellation ring is a Heyting cancellation ring $(A, +, -, 0, \cdot, 1, #)$ that is also a commutative ring.

Examples

• The integers are a commutative Heyting cancellation ring.

• The rational numbers are a commutative Heyting cancellation ring.

• Every commutative discrete cancellation ring is a commutative Heyting cancellation ring.

• Every Heyting integral domain is a commutative Heyting cancellation ring.

• Every commutative Heyting division ring is a commutative Heyting cancellation ring.

• Every commutative Heyting reciprocal ring is a commutative Heyting cancellation ring.

See also

• commutative ring

• commutative cancellation ring