nLab multiplicatively cancellable rig

Definition

Definition

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

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

If RR 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 RR such that for all rRr \in R, if rr is not multiplicatively cancellable, then r=0r = 0.

Definition

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

Definition

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

Last revised on August 3, 2022 at 16:28:29. See the history of this page for a list of all contributions to it.