Prove2Me

Complex_Addition_is_Associative

Proved

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

additionassociativitycomplex-analysisproofwiki

The operation of addition on the set of complex numbers \C\C is associative ∀z1,z2,z3∈\C:z1+\parenz2+z3=\parenz1+z2+z3\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_Addition_is_Associative (z₁ z₂ z₃ : ℂ) : z₁ + z₂ + z₃ = z₁ + (z₂ + z₃) := by sorry
Source
https://proofwiki.org/wiki/Complex_Addition_is_Associative

View graph