Complex_Multiplication_Distributes_over_Addition

Proved

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

complex-additioncomplex-multiplicationdistributive-operationsproofwiki

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

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source

https://proofwiki.org/wiki/Complex_Multiplication_Distributes_over_Addition

View graph