Skip to content
Axiomatic Wiki
Lemma·L45

Elementary consequences of the ring axioms

Zero annihilates products, and negation moves freely across multiplication.

Let be a ring. Then for all : (i) ; (ii) ; (iii) .
In words
In any ring, zero times anything is zero, negating one factor of a product negates the product, and negating both factors leaves the product unchanged.
Rests onF02F05F09F13F14A02
Never needed: F03 · F04 · F06 · F08 · F10 · F11 · F12 · A01 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).

Proof

  1. 1
    (i) using the identity law of D038 and distributivity (R2). Adding to both sides (substitutivity) and using associativity (G1) and the inverse law (G3) of D038: so . Symmetrically, using the other distributive law, .
  2. 2
    (ii) by distributivity, the inverse law of D038, and (i). By uniqueness of inverses in a group (L28), is the inverse of , i.e. . Symmetrically .
  3. 3
    (iii) By (ii) applied twice: . By L28 every group element is the inverse of its own inverse, so .
∎

Remarks

General ring facts, not specific to any one ring; used to verify Bezout's identity and reusable for any future ring built in this library.
Wikipedia ↗mul_zero ↗

Used by

L53L54L59T25T26T28
Propose an edit1 published revision