Integer_Multiplication_is_Associative

Proved

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

associativityinteger-multiplicationproofwiki

The operation of multiplication on the set of integers $\Z$ is associative $\forall x, y, z \in \Z: x \times \paren {y \times z} = \paren {x \times y} \times z$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Integer_Multiplication_is_Associative (a b c : ℤ) : a * (b * c) = a * b * c := by sorry

Source

https://proofwiki.org/wiki/Integer_Multiplication_is_Associative

View graph