# Ring

## Definition 2

$$\forall x,y,z \in S : x + y + z = x + (y + z)$$
$$\forall x,y \in S : x + y = y + x$$
Zero is a right identity element of addition:
$$\forall x \in S : x + 0 = x$$
Zero is a left identity element of addition:
$$\forall x \in S : 0 + x = x$$
Every element has a right additive inverse:
$$\forall x \in S : \exists x' \in S : x + x' = 0$$
Every element has a left additive inverse:
$$\forall x \in S : \exists x' \in S : x' + x = 0$$
Multiplication is associative:
$$\forall x,y,z \in S : xyz = x(yz)$$
$$\forall x,y,z \in S : x(y + z) = xy + xz$$
$$\forall x,y,z \in S : (y + z)x = yx + zx$$

## Axioms

    add_assoc: ?a + ?b + ?c = ?a + (?b + ?c)

add_commute: ?a + ?b = ?b + ?a

add_0_right: ?a + 0 = ?a
add_0: 0 + ?a = ?a

right_minus: ?a + - ?a = 0
left_minus: - ?a + ?a = 0

mult_assoc: ?a * ?b * ?c = ?a * (?b * ?c)

distrib_left: ?a * (?b + ?c) = ?a * ?b + ?a * ?c
distrib_right: (?a + ?b) * ?c = ?a * ?c + ?b * ?c

THEOREM

Zero is a right zero element of multiplication.

$$\forall x \in R : x0 = 0$$

Proof available

THEOREM

Zero is a left zero element of multiplication.

$$\forall x \in R : 0x = 0$$

Proof available

THEOREM    $$(-x) * y = -(x * y)$$

Proof available

THEOREM    $$x * (-y) = -(x * y)$$

Proof available

THEOREM    $$(-x) * (-y) = x * y$$

Proof available

THEOREM    $$-(-x) = x$$

Proof available