ThmDex – An index of mathematical definitions, results, and conjectures.
Formulation F10748 on D610: Real multiplication operation
F10748
Formulation 0
Let $\mathbb{R}$ be the D282: Set of real numbers.
Let $\cdot$ be the D609: Rational multiplication operation.
A D554: Binary operation $* : \mathbb{R} \times \mathbb{R} \to \mathbb{R}$ is a real multiplication operation if and only if
(1) \begin{equation} \forall \, x, y \in [0, \infty) : x * y = 0 \cup \{ a b : 0 \leq a \in x \text{ and } 0 \leq b \in y \} \end{equation}
(2) \begin{equation} \forall \, x, y \in (- \infty, 0) : x * y = (x \cup - x) * (y \cup - y) \end{equation}
(3) \begin{equation} \forall \, x \in [0, \infty) : \forall \, y \in (- \infty, 0) : x * y = - (x \cup - x) * (y \cup - y) \end{equation}