Complex_Multiplication_is_Commutative

Proved

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

complex-multiplicationproofwiki

The operation of multiplication on the set of complex numbers $\C$ is commutative $\forall z_1, z_2 \in \C: z_1 z_2 = z_2 z_1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source