Homotopy Type Theory discrete reciprocal ring > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Definition

< reciprocal ring

A

discrete reciprocal ring is a ring (A,+,,0,,1)(A, +, -, 0, \cdot, 1) with

  • an identity showing that every term not equal to 00 has a reciprocal (a two-sided multiplicative inverse)
    r: (a:A)(((a=0))× (b:A)(ab=1)×(ba=1))r:\prod_{(a:A)} \left( ((a = 0) \to \emptyset) \times \left\Vert \sum_{(b:A)} (a \cdot b = 1) \times (b \cdot a = 1) \right\Vert \right)

Properties

Every discrete reciprocal ring is a discrete division ring.

Examples

See also

Revision on June 12, 2022 at 20:37:46 by Anonymous?. See the history of this page for a list of all contributions to it.