Complex_Multiplication_is_Associative

Proved

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

associativitycomplex-analysismultiplicationproofwiki

The operation of multiplication on the set of complex numbers $\C$ is associative $\forall z_1, z_2, z_3 \in \C: z_1 \paren {z_2 z_3} = \paren {z_1 z_2} z_3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Complex_Multiplication_is_Associative (z₁ z₂ z₃ : ℂ) : z₁ * z₂ * z₃ = z₁ * (z₂ * z₃) := by sorry

Source

https://proofwiki.org/wiki/Complex_Multiplication_is_Associative

View graph