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
Definition D638
Natural number multiplication operation

Let $\mathbb{N}$ be the D225: Set of natural numbers such that
 (i) $x^+$ is a D589: Successor set of $x$ for any $x \in \mathbb{N}$
Let $+$ be the D637: Natural number addition operation.
A D554: Binary operation $\cdot : \mathbb{N} \times \mathbb{N} \to \mathbb{N}$ is a natural number multiplication operation if and only if
 (1) $$\forall \, n \in \mathbb{N} : n \cdot 0 = 0$$ (2) $$\forall \, n, m \in \mathbb{N} : n \cdot m^+ = n \cdot m + n$$
Children
 ▶ D608: Integer multiplication operation