Homotopy Type Theory discrete cancellation ring > history (changes)

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


< integral domain


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

  • a discrete left cancellative identity
    d λ: (a:A)((a=0))× (b:A) (c:A)(ab=ac)(b=c)d_\lambda:\prod_{(a:A)} ((a = 0) \to \emptyset) \times \prod_{(b:A)} \prod_{(c:A)} (a \cdot b = a \cdot c) \implies (b = c)
  • a discrete right cancellative identity
    d λ: (a:A)((a=0))× (b:A) (c:A)(ba=ca)(b=c)d_\lambda:\prod_{(a:A)} ((a = 0) \to \emptyset) \times \prod_{(b:A)} \prod_{(c:A)} (b \cdot a = c \cdot a) \implies (b = c)


See also

Last revised on June 13, 2022 at 01:11:54. See the history of this page for a list of all contributions to it.