Definition:Absolute Value/Ordered Integral Domain

From ProofWiki
Jump to navigation Jump to search


Let $\struct {D, +, \times, \le}$ be an ordered integral domain whose zero is $0_D$.

Then for all $a \in D$, the absolute value of $a$ is defined as:

$\size a = \begin{cases} a & : 0_D \le a \\ -a & : a < 0_D \end{cases}$

where $a > 0_D$ denotes that $\neg \paren {a \le 0_D}$.

Also see

from which it follows that the definition for numbers is compatible with this.