Integer_Multiplication_is_Commutative

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

commutativityinteger-multiplicationproofwiki

The operation of multiplication on the set of integers $\Z$ is commutative $\forall x, y \in \Z: x \times y = y \times x$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Integer_Multiplication_is_Commutative (a b : ℤ) : a * b = b * a := by sorry

Source