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
Complex multiplication operation