## Definition ## A __discrete cancellation ring__ is a [[ring]] $(A, +, -, 0, \cdot)$ with * a discrete left cancellative identity $$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_\lambda:\prod_{(a:A)} ((a = 0) \to \emptyset) \times \prod_{(b:A)} \prod_{(c:A)} (b \cdot a = c \cdot a) \implies (b = c)$$ ## Examples ## * The [[integers]] are a discrete cancellation ring. * The [[rational numbers]] are a discrete cancellation ring. * Every [[discrete domain]] is a discrete cancellation ring. * Every [[discrete division ring]] is a discrete cancellation ring. * Every [[discrete reciprocal ring]] is a discrete cancellation ring. ## See also ## * [[ring]] * [[cancellation ring]]