Skip to content
Axiomatic Wiki
Lemma·L12

Commutativity of multiplication

Order does not matter when multiplying.

for all .
In words
The product of m and n equals the product of n and m, for all natural numbers m and n.
Rests onF02F09F14A01A06
Never needed: F03 · F04 · F05 · F06 · F08 · F10 · F11 · F12 · F13 · A02 · A03 · A04 · A05 · A07 · A08 (computed from the citation graph, not asserted).

Proof

  1. 1
    Fix and induct on (T05, Separation).
  2. 2
    Base: by D028, and by Claim A of L11; so .
  3. 3
    Step: assume . Then by D028, the hypothesis with substitutivity, and Claim B of L11 read right to left.
∎

Remarks

With associativity and the unit (note by D028 (twice) and Claim A), the naturals under multiplication form a commutative monoid as well.
Wikipedia ↗Nat.mul_comm ↗

Used by

L13L19L21L35L40L44L46T10T13T19T23
Propose an edit1 published revision