ThmDex – An index of mathematical definitions, results, and conjectures.
▼ Set of symbols
▼ Alphabet
▼ Deduction system
▼ Theory
▼ Zermelo-Fraenkel set theory
▼ Set
▼ Binary cartesian set product
▼ Binary relation
▼ Map
▼ Operation
▼ N-operation
▼ Binary operation
▼ Enclosed binary operation
▼ Groupoid
▼ Ringoid
▼ Semiring
▼ Ring
▼ Multiplicative group
▼ Multiplicative monoid
▼ Multiplicative semigroup
▼ Multiplicative groupoid
▼ Multiplicative binary operation
▼ Natural number multiplication operation
▼ Integer multiplication operation
▼ Rational multiplication operation
Definition D610
Real multiplication operation
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}
Children
▶ D611: Complex multiplication operation