ThmDex – An index of mathematical definitions, results, and conjectures.
Formulation F349 on D559: Semiring
F349
Formulation 0
An D21: Algebraic structure $R = (X, +, \times)$ is a semiring if and only if
(1) $\forall \, x, y \in X : x + y \in X$ (D20: Enclosed binary operation)
(2) $\forall \, x, y \in X : x y \in X$ (D20: Enclosed binary operation)
(3) $\forall \, x, y, z \in X : x (y + z) = (x y) + (x z)$ (D555: Left-distributive binary operation)
(4) $\forall \, x, y, z \in X : (x + y) z = (x z) + (y z)$ (D556: Right-distributive binary operation)
(5) $\forall \, x, y, z \in X : x + (y + z) = (x + y) + z$ (D488: Associative binary operation)
(6) $\forall \, x, y, z \in X : x (y z) = (x y) z$ (D488: Associative binary operation)