Complex_Addition_is_Commutative

Proved

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

additioncommutativitycomplex-analysisproofwiki

The operation of addition on the set of complex numbers is commutative $\forall z, w \in \C: z + w = w + z$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Complex_Addition_is_Commutative (z w : ℂ) : z + w = w + z := by sorry

Source