nLab multiplicatively cancellable rig

Definition

In classical mathematics, a multiplicatively cancellable rig is a rig $R$ such that each $(r \neq 0) \in R$ is multiplicatively cancellable.

An element $r \in R$ where $R$ is a rig is left multiplicatively cancellable iff for every $s,t \in R$ we have that $(r.s = r.t) \Rightarrow (s = t)$ and it is right multiplicatively cancellable iff for every $s,t \in R$ we have that $(s.r = t.r) \Rightarrow (s = t)$. An element $r \in R$ is multiplicatively cancellable iff it is left multiplicatively cancellable and right multiplicatively cancellable.

If $R$ is a commutative rig, an element is left multiplicatively cancellable iff it is right multiplicatively cancellable.

In constructive mathematics

Like in the case for integral domains and fields, the definition above bifurcates into multiple definitions in constructive mathematics.

definitions to be ported over

Definition

A residue multiplicatively cancellable rig is a rig $R$ such that for all $r \in R$, if $r$ is not multiplicatively cancellable, then $r = 0$.

Definition

A Heyting multiplicatively cancellable rig is a rig $R$ with a tight apartness relation $\#$ such that each $(r \# 0) \in R$ is multiplicatively cancellable.

Definition

A discrete multiplicatively cancellable rig is a rig $R$ such that each $r \in R$ is zero xor multiplicatively cancellable.