Complex numbers · The Lumenary

Lens

MotivationH

A square root that would not go away

In 1545 Gerolamo Cardano published a formula for solving cubic equations. For an equation $x^3 = px + q$ it reads

x = \sqrt[3]{\frac q2 + \sqrt{\frac{q^2}{4} - \frac{p^3}{27}}} + \sqrt[3]{\frac q2 - \sqrt{\frac{q^2}{4} - \frac{p^3}{27}}}.

Rafael Bombelli tried it on $x^3 = 15x + 4$ , which obviously has the solution $x = 4$ (since $64 = 60 + 4$ ). The formula gives

x = \sqrt[3]{2 + \sqrt{-121}} + \sqrt[3]{2 - \sqrt{-121}}.

A square root of a negative number! Bombelli did not give up. In his Algebra (1572) he calculated boldly with a "number" $\sqrt{-1}$ obeying the usual rules plus $\big(\sqrt{-1}\big)^2 = -1$ , and noticed that $\big(2 + \sqrt{-1}\big)^3 = 2 + 11\sqrt{-1} = 2 + \sqrt{-121}$ . So the two cube roots are $2 + \sqrt{-1}$ and $2 - \sqrt{-1}$ , and their sum is $4$ . The "impossible" numbers were needed to reach a perfectly real answer.

Today these numbers are indispensable: electrical engineers use them for alternating currents, physicists write quantum mechanics with them, and the images of the Mandelbrot set are pictures of complex arithmetic. In this lesson we build them carefully, see what they look like, and prove their main properties.

IntuitionH

Numbers you can turn

Think of multiplication by $-1$ as a motion of the number line: it swaps $3$ and $-3$ , $1$ and $-1$ — it is a half turn about $0$ . Doing it twice is a full turn: $(-1)(-1) = 1$ .

Now ask for a number $i$ with $i^2 = -1$ : "multiplying by $i$ twice is a half turn". On the line that is impossible. But in the plane there is an obvious candidate: a quarter turn about $0$ . Two quarter turns make a half turn. So we let numbers live in a plane: the real numbers along the horizontal axis, and $i$ one unit up. Then $1 \xrightarrow{\times i} i \xrightarrow{\times i} -1 \xrightarrow{\times i} -i \xrightarrow{\times i} 1$ walks around a square.

DefinitionsH

Definitions

Definition— complex number

A complex number is an expression $z = a + bi$ with $a, b \in \R$ . The number $a = \operatorname{Re} z$ is its real part and $b = \operatorname{Im} z$ its imaginary part; two complex numbers are equal when their real parts are equal and their imaginary parts are equal. The set of complex numbers is $\C$ . We identify the real number $a$ with $a + 0i$ , so $\R \subseteq \C$ .

Arithmetic follows the usual rules of algebra together with $i^2 = -1$ :

(a + bi) + (c + di) = (a + c) + (b + d)i, \qquad (a + bi)(c + di) = (ac - bd) + (ad + bc)i.

(Expand the product and replace $bd\,i^2$ by $-bd$ .) Formally one can define $\C$ as the set of pairs $(a, b)$ of reals with these two operations and check every law of arithmetic — commutativity, associativity, distributivity — directly. That is how Hamilton defined complex numbers in 1837, and how Mathlib defines them.

Definition— complex plane

The complex number $a + bi$ is drawn as the point $(a, b)$ — or the arrow from $0$ to it — in the complex plane (also called an Argand diagram). The horizontal axis is the real axis, the vertical axis the imaginary axis.

Definition— conjugate, modulus and argument

For $z = a + bi$ :

the conjugate is $\bar z = a - bi$ , the mirror image of $z$ in the real axis;
the modulus is $|z| = \sqrt{a^2 + b^2}$ , the distance from $0$ to $z$ (Pythagoras);
for $z \ne 0$ , an argument $\arg z$ is an angle $\theta$ from the positive real axis to the arrow $0z$ , measured anticlockwise in radians. It is defined only up to adding multiples of $2\pi$ ; the principal argument is the one in $(-\pi, \pi]$ . The number $0$ has no argument.

Definition— polar form

If $|z| = r$ and $\theta$ is an argument of $z$ , then $a = r\cos\theta$ and $b = r\sin\theta$ , so

z = r(\cos\theta + i \sin\theta) = r \operatorname{cis}\theta, \qquad \text{where } \operatorname{cis}\theta = \cos\theta + i\sin\theta.

This is the polar form of $z$ . The number $\operatorname{cis}\theta$ is the point at angle $\theta$ on the unit circle $|z| = 1$ .

You need the trigonometry of the unit circle and the addition formulas from Trigonometry, and the quadratic formula from Quadratic equations.

Worked examplesH

Worked examples

Example— Arithmetic

$(3 + 2i) + (1 - 4i) = 4 - 2i$ .
$(3 + 2i)(1 - 4i) = 3 - 12i + 2i - 8i^2 = 3 - 10i + 8 = 11 - 10i$ .
Powers of $i$ repeat with period $4$ : $i^1 = i$ , $i^2 = -1$ , $i^3 = -i$ , $i^4 = 1$ , $i^5 = i, \dots$ So $i^{2026} = i^{4 \cdot 506 + 2} = i^2 = -1$ .

Example— Division with the conjugate

To divide, multiply the top and bottom by the conjugate of the bottom, which makes the bottom real:

\frac{3 + 4i}{1 + 2i} = \frac{(3 + 4i)(1 - 2i)}{(1 + 2i)(1 - 2i)} = \frac{3 - 6i + 4i - 8i^2}{1 - 4i^2} = \frac{11 - 2i}{5} = \frac{11}{5} - \frac25 i.

In general $z \bar z = (a + bi)(a - bi) = a^2 + b^2 = |z|^2$ , so $\dfrac1z = \dfrac{\bar z}{|z|^2}$ for every $z \ne 0$ . Every non-zero complex number has an inverse: $\C$ is a field.

Example— Polar forms

$1 + i$ : modulus $\sqrt{1 + 1} = \sqrt 2$ , argument $\tfrac\pi4$ , so $1 + i = \sqrt 2 \operatorname{cis}\tfrac\pi4$ .
$-1 = \operatorname{cis}\pi$ , and $i = \operatorname{cis}\tfrac\pi2$ .
$-\sqrt 3 + i$ : modulus $\sqrt{3 + 1} = 2$ ; the point is in the second quadrant with $\cos\theta = -\tfrac{\sqrt3}2$ , $\sin\theta = \tfrac12$ , so $\theta = \tfrac{5\pi}{6}$ and $-\sqrt 3 + i = 2\operatorname{cis}\tfrac{5\pi}6$ .
Careful: $\tan\theta = \tfrac ba$ alone does not determine $\theta$ . For $-1 - i$ , $\tfrac ba = 1$ , but the point is in the third quadrant: its principal argument is $-\tfrac{3\pi}{4}$ , not $\tfrac\pi4$ .

Explore

Explore: arithmetic as geometry

Drag $z$ and $w$ . Addition is the parallelogram rule — complex numbers add like arrows (vectors). Then switch to the product: watch the lengths multiply and the angles add.

Multiplying complex numbers

Compare |zw| with |z||w|, and arg(zw) with arg z + arg w. Then try the quotient and the conjugate.

Drag the points, or focus one with Tab and use the arrow keys (hold Shift for small steps).

z =Re+Imi

w =Re+Imi

	Number	Modulus	Argument
z	1.5 + 0.5i	1.581	18.4°0.322 rad
w	0.5 + i	1.118	63.4°1.107 rad
zw	0.25 + 1.75i	1.768	81.9°1.429 rad

Lengths multiply: 1.581 × 1.118 = 1.768

Angles add: 18.4° + 63.4° = 81.9°

Multiplying by w stretches by |w| and turns by arg w: lengths multiply and angles add.

Multiplication by a fixed number $w = a + bi$ moves the whole plane: it rotates by $\arg w$ and scales by $|w|$ . As a map of the plane $(x, y) \mapsto (ax - by,\, bx + ay)$ it is the matrix $\begin{pmatrix} a & -b \\ b & a \end{pmatrix}$ . Here is multiplication by $1 + i$ : a rotation by $45^\circ$ and a stretch by $\sqrt 2$ .

Multiplication by 1 + i

The determinant is a² + b² = |w|². Which matrices of the form [[a, −b], [b, a]] are pure rotations?

Your own matrix

image of the grid
image of the unit square
image of the flag
before the transformation

From the identity I to As = 1

A =

The columns of A are the images of e₁ = (1, 0) and e₂ = (0, 1): Ae₁ = (1, 1), Ae₂ = (−1, 1)

det A = ad − bc = 2

The unit square (area 1) becomes a parallelogram of area |det A| = 2. Since det A > 0, orientation is preserved.

Invariant lines (real eigenvectors)

λ = 1 ± 1i

No real eigenvectors: A turns every direction, so no line through 0 stays put. The eigenvalues are complex.

ProofH

Theorems and proofs

Theorem— Theorem 1 (moduli multiply)

For all complex numbers $z, w$ : $\;|zw| = |z|\,|w|$ .

Proof

Write $z = a + bi$ , $w = c + di$ , so $zw = (ac - bd) + (ad + bc)i$ . Expanding both sides shows the two-squares identity

(a^2 + b^2)(c^2 + d^2) = (ac - bd)^2 + (ad + bc)^2,

since both sides equal $a^2c^2 + a^2d^2 + b^2c^2 + b^2d^2$ (the cross terms $\mp 2abcd$ cancel on the right). That says $|z|^2 |w|^2 = |zw|^2$ . Taking non-negative square roots gives $|zw| = |z|\,|w|$ .

∎

Theorem— Theorem 2 (multiplication in polar form)

For all real $\alpha, \beta$ : $\;\operatorname{cis}\alpha \cdot \operatorname{cis}\beta = \operatorname{cis}(\alpha + \beta)$ . Consequently

r\operatorname{cis}\alpha \cdot s\operatorname{cis}\beta = rs\operatorname{cis}(\alpha + \beta):

to multiply complex numbers, multiply the moduli and add the arguments.

Proof

By the multiplication rule,

(\cos\alpha + i\sin\alpha)(\cos\beta + i\sin\beta) = (\cos\alpha\cos\beta - \sin\alpha\sin\beta) + i(\sin\alpha\cos\beta + \cos\alpha\sin\beta).

By the addition formulas of trigonometry the real part is $\cos(\alpha + \beta)$ and the imaginary part is $\sin(\alpha + \beta)$ . The second statement follows by multiplying by $rs$ .

∎

So the addition formulas for sine and cosine are "really" the statement that angles add when complex numbers multiply. In particular $\operatorname{cis}\theta \cdot \operatorname{cis}(-\theta) = \operatorname{cis} 0 = 1$ , so $\operatorname{cis}(-\theta) = (\operatorname{cis}\theta)^{-1}$ ; it is also the conjugate $\overline{\operatorname{cis}\theta}$ .

Theorem— Theorem 3 (De Moivre)

For every real $\theta$ and every integer $n$ :

(\cos\theta + i\sin\theta)^n = \cos n\theta + i\sin n\theta.

Proof

First let $n \ge 0$ ; we use induction on $n$ . For $n = 0$ both sides are $1$ . If $\operatorname{cis}^k\theta = \operatorname{cis}(k\theta)$ , then by Theorem 2

\operatorname{cis}^{k+1}\theta = \operatorname{cis}^k\theta \cdot \operatorname{cis}\theta = \operatorname{cis}(k\theta)\operatorname{cis}\theta = \operatorname{cis}\big((k + 1)\theta\big).

For negative $n = -m$ with $m > 0$ : $\operatorname{cis}^{-m}\theta = \big(\operatorname{cis}^m\theta\big)^{-1} = \big(\operatorname{cis}(m\theta)\big)^{-1} = \operatorname{cis}(-m\theta)$ , using the remark after Theorem 2.

∎

De Moivre's theorem turns powers into multiplication of angles. Expanding $(\cos\theta + i\sin\theta)^3$ with the binomial theorem and comparing real parts gives $\cos 3\theta = 4\cos^3\theta - 3\cos\theta$ — a trigonometric identity obtained by pure algebra (the experiment below lets SymPy do it).

Theorem— Theorem 4 (roots of unity)

Let $n \ge 1$ . The equation $z^n = 1$ has exactly $n$ complex solutions,

\omega_k = \operatorname{cis}\frac{2\pi k}{n}, \qquad k = 0, 1, \dots, n - 1,

the $n$ -th roots of unity. They are the vertices of a regular $n$ -gon inscribed in the unit circle, with one vertex at $1$ . For $n \ge 2$ they add up to $0$ .

Proof

Each $\omega_k$ is a solution: by De Moivre, $\omega_k^n = \operatorname{cis}(2\pi k) = \cos 2\pi k + i \sin 2\pi k = 1$ .

There are no others: if $z^n = 1$ then $|z|^n = |z^n| = 1$ by Theorem 1, so $|z| = 1$ and $z = \operatorname{cis}\theta$ for some $\theta$ . De Moivre gives $\cos n\theta + i\sin n\theta = 1$ , so $\cos n\theta = 1$ , which forces $n\theta = 2\pi k$ for an integer $k$ , i.e. $\theta = \tfrac{2\pi k}{n}$ . Since $\operatorname{cis}$ repeats with period $2\pi$ , only $k = 0, \dots, n - 1$ give different numbers, and these $n$ angles all lie in $[0, 2\pi)$ , so they give $n$ distinct points.

Regular polygon: consecutive $\omega_k$ are at angles differing by $\tfrac{2\pi}{n}$ on the unit circle.

Sum: let $\omega = \omega_1 \ne 1$ (as $n \ge 2$ ), so $\omega_k = \omega^k$ . The geometric sum $S = 1 + \omega + \dots + \omega^{n-1}$ satisfies $(\omega - 1)S = \omega^n - 1 = 0$ , and $\omega - 1 \ne 0$ , so $S = 0$ .

∎

The same idea finds all $n$ -th roots of any non-zero $w = R\operatorname{cis}\varphi$ : they are $R^{1/n}\operatorname{cis}\dfrac{\varphi + 2\pi k}{n}$ for $k = 0, \dots, n - 1$ , again a regular $n$ -gon. For example the square roots of $i = \operatorname{cis}\tfrac\pi2$ are $\pm\operatorname{cis}\tfrac\pi4 = \pm\tfrac{1 + i}{\sqrt 2}$ .

The sixth roots of unity

Change n, then move c away from 1 to see the n-th roots of other numbers.

Number of roots nn = 6

Try

Drag the points, or focus one with Tab and use the arrow keys (hold Shift for small steps).

c =Re+Imi

Solutions of wⁿ = c for n = 6:

w₀ = 1
w₁ = 0.5 + 0.866i
w₂ = −0.5 + 0.866i
w₃ = −1
w₄ = −0.5 − 0.866i
w₅ = 0.5 − 0.866i

All roots lie on the circle of radius |c|^(1/n) ≈ 1.

Neighbouring roots are 60° apart: 360° ÷ 6.

w₀ is the principal root, at the angle (arg c)/n; the others follow by equal turns.

Because c = 1, these are the roots of unity of order 6.

The roots add up to 0, so the regular polygon is balanced around the origin.

Theorem— Theorem 5 (quadratics with negative discriminant)

Let $a, b, c$ be real, $a \ne 0$ , and $\Delta = b^2 - 4ac < 0$ . Then $az^2 + bz + c = 0$ has the two complex solutions

z = \frac{-b \pm i\sqrt{-\Delta}}{2a},

which are conjugates of each other.

Proof

Let $s = \sqrt{-\Delta} = \sqrt{4ac - b^2}$ , a positive real number, and $z = \tfrac{-b + is}{2a}$ . Put $w = 2az = -b + is$ . Multiplying the equation by $4a$ ,

4a(az^2 + bz + c) = (2az)^2 + 2b(2az) + 4ac = w^2 + 2bw + 4ac.

Now $w^2 = b^2 - 2bsi + s^2 i^2 = b^2 - 2bsi - s^2$ and $2bw = -2b^2 + 2bsi$ , so $w^2 + 2bw + 4ac = -b^2 - s^2 + 4ac = 0$ , because $s^2 = 4ac - b^2$ . As $4a \ne 0$ , $az^2 + bz + c = 0$ . The other root is obtained by replacing $s$ with $-s$ , which conjugates $z$ .

∎

For example $z^2 + 2z + 5 = 0$ has $\Delta = 4 - 20 = -16$ , so $z = \tfrac{-2 \pm 4i}{2} = -1 \pm 2i$ . Check: $(-1 + 2i)^2 + 2(-1 + 2i) + 5 = (1 - 4i - 4) + (-2 + 4i) + 5 = 0$ .

Quadratics are only the beginning:

Theorem— Fundamental theorem of algebra (statement)

Every non-constant polynomial with complex coefficients has at least one complex root. Consequently a polynomial of degree $n \ge 1$ factors into $n$ linear factors over $\C$ .

We do not prove it here: every proof needs a substantial idea from analysis or topology (a sketch of one appears among the viewpoints below). It is why the complex numbers are the natural home of algebra: inventing $i$ to solve $x^2 + 1 = 0$ turns out to make every polynomial equation solvable.

Finally, one thing is lost. The real numbers are ordered compatibly with arithmetic: positive times positive is positive, and every non-zero number is positive or negative, but not both. Not so for $\C$ .

Theorem— Theorem 6 (ℂ cannot be ordered)

There is no set $P \subseteq \C$ ("the positive numbers") such that products of elements of $P$ lie in $P$ and every $z \ne 0$ satisfies exactly one of $z \in P$ , $-z \in P$ .

Proof

Suppose $P$ were such a set. Since $i \ne 0$ , either $i \in P$ or $-i \in P$ . In the first case $i \cdot i = -1 \in P$ ; in the second $(-i)(-i) = i^2 = -1 \in P$ . Either way $-1 \in P$ . Then $1 = (-1)(-1) \in P$ too. But then both $1$ and $-1 = -(1)$ are in $P$ , which is forbidden.

∎

So statements like " $i > 0$ " or " $2 + i < 3$ " have no meaning in $\C$ . We can compare moduli — $|2 + i| = \sqrt5 < 3$ — because those are real numbers.

Formal mathematicsF

Complex numbers in Lean

Mathlib defines ℂ as pairs of real numbers ⟨re, im⟩, with I = ⟨0, 1⟩, and proves that it is a field. So $i^2 = -1$ is a theorem, not an assumption:

i_sqLean 4Applies a library theoremFormally verified

/-- The defining property of `i`: `i² = -1`. This applies Mathlib's `Complex.I_sq`; in Mathlib,
`I` is the pair `⟨0, 1⟩` and the equation is a computation with the multiplication rule for
pairs. -/
theorem i_sq : I ^ 2 = -1 := Complex.I_sq

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

The multiplication rule and our division example. The tactic linear_combination checks that two sides differ by a multiple of $i^2 + 1$ , which is exactly "replace $i^2$ by $-1$ ":

mul_ruleLean 4Proved here from basic factsFormally verified

/-- **The multiplication rule.** `(a + bi)(c + di) = (ac − bd) + (ad + bc)i`: expand with the
distributive law and replace `i²` by `-1`. The `linear_combination` step says precisely that
the two sides differ by `bd (i² + 1)`, which is `0`. -/
theorem mul_rule (a b c d : ℝ) :
    ((a : ℂ) + b * I) * (c + d * I) = (a * c - b * d) + (a * d + b * c) * I := by
  linear_combination ((b : ℂ) * d) * I_sq

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

div_exampleLean 4Proved here from basic factsFormally verified

/-- **Division by the conjugate trick.** `(3 + 4i)/(1 + 2i) = 11/5 − (2/5) i`, because
`(3 + 4i)(1 − 2i) = 11 − 2i` and `(1 + 2i)(1 − 2i) = 5`. Lean checks the equivalent statement
`3 + 4i = (11/5 − (2/5)i)(1 + 2i)`. -/
theorem div_example : (3 + 4 * I) / (1 + 2 * I) = 11 / 5 - 2 / 5 * I := by
  have h : (1 + 2 * I) ≠ 0 := by
    intro h
    have := congrArg Complex.re h
    simp at this
  rw [div_eq_iff h]
  linear_combination (4 / 5 : ℂ) * I_sq

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

mul_conjLean 4Applies a library theoremFormally verified

/-- `z · z̄ = |z|²`, a real number: this is why multiplying by the conjugate clears
denominators. Mathlib's `Complex.mul_conj` states it with `normSq z = a² + b²`. -/
theorem mul_conj (z : ℂ) : z * (starRingEnd ℂ) z = (normSq z : ℂ) := Complex.mul_conj z

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

Theorem 1, via the two-squares identity. Mathlib writes normSq z for $|z|^2 = a^2 + b^2$ and ‖z‖ for the modulus $|z|$ :

two_squares_identityLean 4Proved here from basic factsFormally verified

/-- **The two-squares identity** (Brahmagupta; Fibonacci's *Liber Quadratorum*):
`(a² + b²)(c² + d²) = (ac − bd)² + (ad + bc)²`. A product of two sums of two squares is again a
sum of two squares. It holds in every commutative ring; `ring` checks it. -/
theorem two_squares_identity {R : Type*} [CommRing R] (a b c d : R) :
    (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2) = (a * c - b * d) ^ 2 + (a * d + b * c) ^ 2 := by
  ring

Axioms used: propext, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

normSq_mulLean 4Proved here from basic factsFormally verified

/-- **`|zw|² = |z|² |w|²`.** With `z = a + bi` and `w = c + di`, `zw = (ac − bd) + (ad + bc)i`,
so this *is* the two-squares identity. (Mathlib: `Complex.normSq_mul`.) -/
theorem normSq_mul (z w : ℂ) : normSq (z * w) = normSq z * normSq w := by
  simp only [normSq_apply, mul_re, mul_im]
  ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

norm_mulLean 4Applies a library theoremFormally verified

/-- **Moduli multiply:** `|zw| = |z| |w|` (Mathlib writes `‖z‖` for the modulus). This applies
Mathlib's `Complex.norm_mul`; it follows from `normSq_mul` by taking square roots. -/
theorem norm_mul (z w : ℂ) : ‖z * w‖ = ‖z‖ * ‖w‖ := Complex.norm_mul z w

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

Mathlib has no cis, so we define it, prove that it lies on the unit circle and that it turns multiplication into addition of angles (Theorem 2), and prove De Moivre's theorem by induction for natural numbers $n$ (the extension to negative $n$ is not formalised here):

cisLean 4Formally verified

/-- `cis θ = cos θ + i sin θ`, the point at angle `θ` on the unit circle. A number with modulus
`r` and argument `θ` is `r · cis θ`. (Mathlib has no `cis`; it uses `exp (θ * I)`, see
`cis_eq_exp`.) -/
noncomputable def cis (θ : ℝ) : ℂ := Real.cos θ + Real.sin θ * I

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

norm_cisLean 4Proved here from basic factsFormally verified

/-- `cis θ` lies on the unit circle: `|cis θ| = √(cos² θ + sin² θ) = 1`. -/
theorem norm_cis (θ : ℝ) : ‖cis θ‖ = 1 := by
  rw [cis, Complex.norm_add_mul_I]
  simp [Real.cos_sq_add_sin_sq]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

cis_addLean 4Proved here from basic factsFormally verified

/-- **Multiplying adds angles:** `cis (α + β) = cis α · cis β`. Expand the right side with the
multiplication rule: its real part is `cos α cos β − sin α sin β = cos (α + β)` and its
imaginary part is `sin α cos β + cos α sin β = sin (α + β)` — the addition formulas of
trigonometry. -/
theorem cis_add (α β : ℝ) : cis (α + β) = cis α * cis β := by
  simp only [cis, Real.cos_add, Real.sin_add, Complex.ofReal_add, Complex.ofReal_mul,
    Complex.ofReal_sub]
  linear_combination (-(Real.sin α : ℂ) * Real.sin β) * I_sq

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

polar_mulLean 4Proved here from basic factsFormally verified

/-- **Multiplication in polar form:** `(r cis α)(s cis β) = (rs) cis (α + β)`. Moduli multiply
and arguments add: a rotation combined with a scaling. -/
theorem polar_mul (r s α β : ℝ) :
    ((r : ℂ) * cis α) * ((s : ℂ) * cis β) = ((r * s : ℝ) : ℂ) * cis (α + β) := by
  rw [cis_add]
  push_cast
  ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

de_moivreLean 4Proved here from basic factsFormally verified

/-- **De Moivre's theorem:** `(cos θ + i sin θ)ⁿ = cos nθ + i sin nθ` for every natural number
`n`. Induction on `n`: the case `0` is `1 = cis 0`, and
`cis θ ^ (k + 1) = cis θ ^ k · cis θ = cis (kθ) · cis θ = cis (kθ + θ)` by `cis_add`.
(Mathlib: `Complex.cos_add_sin_mul_I_pow`.) -/
theorem de_moivre (θ : ℝ) (n : ℕ) : cis θ ^ n = cis (n * θ) := by
  induction n with
  | zero => simp [cis]
  | succ k ih =>
    rw [pow_succ, ih, ← cis_add]
    congr 1
    push_cast
    ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

cis_eq_expLean 4Applies a library theoremFormally verified

/-- **Euler's formula** `e^{iθ} = cos θ + i sin θ`: our `cis θ` is Mathlib's `exp (θ * I)`.
This applies `Complex.exp_mul_I` and the fact that `cos` and `sin` of a real number are real. -/
theorem cis_eq_exp (θ : ℝ) : cis θ = Complex.exp (θ * I) := by
  rw [Complex.exp_mul_I, cis, Complex.ofReal_cos, Complex.ofReal_sin]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

Roots of unity. We prove that each $\operatorname{cis}\tfrac{2\pi k}{n}$ is an $n$ -th root of unity and that roots of unity other than $1$ sum to $0$ ; that there are exactly $n$ of them we take from Mathlib, whose rootsOfUnity n ℂ is the group of all $\zeta$ with $\zeta^n = 1$ :

cis_root_of_unityLean 4Proved here from basic factsFormally verified

/-- **`cis (2πk/n)` is an `n`-th root of unity.** By De Moivre,
`cis (2πk/n) ^ n = cis (2πk) = cos 2πk + i sin 2πk = 1`. Together with `norm_cis`, the `n`
numbers `cis (2πk/n)`, `k = 0, …, n − 1`, sit on the unit circle at equal angles `2π/n`:
the vertices of a regular `n`-gon. -/
theorem cis_root_of_unity (n k : ℕ) (hn : n ≠ 0) : cis (2 * Real.pi * k / n) ^ n = 1 := by
  rw [de_moivre]
  have h : (n : ℝ) * (2 * Real.pi * k / n) = k * (2 * Real.pi) := by
    field_simp
  have hsin : Real.sin (k * (2 * Real.pi)) = 0 := by
    rw [show (k : ℝ) * (2 * Real.pi) = ((2 * k : ℕ) : ℝ) * Real.pi by push_cast; ring]
    exact Real.sin_nat_mul_pi _
  rw [h, cis, Real.cos_nat_mul_two_pi, hsin]
  simp

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

sum_roots_of_unityLean 4Proved here from basic factsFormally verified

/-- **The `n`-th roots of unity add up to `0`.** If `ω ^ n = 1` and `ω ≠ 1`, then
`1 + ω + ⋯ + ω^(n−1) = 0`: multiplying the sum by `ω − 1` telescopes to `ωⁿ − 1 = 0`
(Mathlib's `geom_sum_mul`), and `ω − 1 ≠ 0`. With `ω = cis (2π/n)` this says the vertices of a
regular `n`-gon centred at `0` balance at the centre. -/
theorem sum_roots_of_unity {ω : ℂ} {n : ℕ} (hω : ω ^ n = 1) (h1 : ω ≠ 1) :
    ∑ k ∈ Finset.range n, ω ^ k = 0 := by
  have h := geom_sum_mul ω n
  rw [hω, sub_self] at h
  exact (mul_eq_zero.mp h).resolve_right (sub_ne_zero.mpr h1)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

card_roots_of_unityLean 4Applies a library theoremFormally verified

/-- **There are exactly `n` complex `n`-th roots of unity** (for `n ≥ 1`). This applies
Mathlib's `Complex.card_rootsOfUnity`; `rootsOfUnity n ℂ` is the group of units `ζ` with
`ζ ^ n = 1`. -/
theorem card_roots_of_unity (n : ℕ) [NeZero n] : Nat.card (rootsOfUnity n ℂ) = n :=
  Complex.card_rootsOfUnity n

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

Quadratics with negative discriminant (Theorem 5), and the fundamental theorem of algebra, which Mathlib proves using complex analysis:

quadratic_exampleLean 4Proved here from basic factsFormally verified

/-- `z² + 2z + 5 = 0` has discriminant `4 − 20 = −16 < 0`, so no real roots — but
`z = −1 + 2i` is a complex root: `(−1 + 2i)² + 2(−1 + 2i) + 5 = 4 + 4i² = 0`. -/
theorem quadratic_example : (-1 + 2 * I) ^ 2 + 2 * (-1 + 2 * I) + 5 = 0 := by
  linear_combination (4 : ℂ) * I_sq

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

quadratic_formula_neg_discLean 4Proved here from basic factsFormally verified

/-- **The quadratic formula when `Δ = b² − 4ac < 0`.** With `s = √(4ac − b²)` (a real number),
`z = (−b + s i)/(2a)` solves `az² + bz + c = 0`. Proof: put `w = 2az = −b + si`; then
`4a(az² + bz + c) = w² + 2bw + 4ac = −b² + s² i² + 4ac = −b² − s² + 4ac = 0`. -/
theorem quadratic_formula_neg_disc (a b c : ℝ) (ha : a ≠ 0) (hΔ : b ^ 2 - 4 * a * c < 0)
    (z : ℂ) (hz : z = (-b + Real.sqrt (4 * a * c - b ^ 2) * I) / (2 * a)) :
    a * z ^ 2 + b * z + c = 0 := by
  set s := Real.sqrt (4 * a * c - b ^ 2) with hsdef
  have hs : s ^ 2 = 4 * a * c - b ^ 2 := Real.sq_sqrt (by linarith)
  have hs' : (s : ℂ) ^ 2 = 4 * a * c - b ^ 2 := by exact_mod_cast hs
  have ha' : (a : ℂ) ≠ 0 := by exact_mod_cast ha
  have hw : 2 * (a : ℂ) * z = -b + s * I := by
    rw [hz]
    field_simp
  have h4 : 4 * (a : ℂ) * (a * z ^ 2 + b * z + c) = 0 := by
    linear_combination (2 * a * z + (-b + s * I) + 2 * b) * hw + (s : ℂ) ^ 2 * I_sq - hs'
  have h4a : (4 * (a : ℂ)) ≠ 0 := mul_ne_zero (by norm_num) ha'
  exact (mul_eq_zero.mp h4).resolve_left h4a

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

fundamental_theorem_of_algebraLean 4Applies a library theoremFormally verified

/-- **The fundamental theorem of algebra:** every non-constant polynomial with complex
coefficients has a complex root. This applies Mathlib's `Complex.exists_root`, whose proof
uses analysis (Liouville's theorem), well beyond this lesson. -/
theorem fundamental_theorem_of_algebra {f : Polynomial ℂ} (hf : 0 < f.degree) :
    ∃ z : ℂ, f.IsRoot z :=
  Complex.exists_root hf

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

And Theorem 6. An ordering compatible with arithmetic is described by its set P of positive elements, so "no such P" is the formal content of "ℂ cannot be ordered":

no_positive_coneLean 4Proved here from basic factsFormally verified

/-- **ℂ cannot be made into an ordered field.** An ordering compatible with arithmetic is the
same as a set `P` of "positive" numbers closed under multiplication, such that every `z ≠ 0`
has `z ∈ P` or `-z ∈ P`, but never both. No such `P` exists in `ℂ`: whether `i ∈ P` or
`-i ∈ P`, the product of that number with itself is `i² = (-i)² = -1`, so `-1 ∈ P`; then
`1 = (-1)(-1) ∈ P` as well — but `1` and `-1` cannot both be positive. -/
theorem no_positive_cone (P : Set ℂ) (mul_mem : ∀ a b, a ∈ P → b ∈ P → a * b ∈ P)
    (total : ∀ z : ℂ, z ≠ 0 → z ∈ P ∨ -z ∈ P) (not_both : ∀ z : ℂ, z ∈ P → -z ∉ P) :
    False := by
  have hm1 : (-1 : ℂ) ∈ P := by
    rcases total I I_ne_zero with h | h
    · have := mul_mem _ _ h h
      rwa [← sq, I_sq] at this
    · have := mul_mem _ _ h h
      rwa [neg_mul_neg, ← sq, I_sq] at this
  have h1 : (1 : ℂ) ∈ P := by
    have := mul_mem _ _ hm1 hm1
    rwa [neg_mul_neg, one_mul] at this
  exact not_both 1 h1 hm1

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ComplexNumbers.leanTry it in the Lean web editor

(Mathlib does put a partial order on ℂ, available after open scoped ComplexOrder: $z \le w$ means $\operatorname{Re} z \le \operatorname{Re} w$ and $\operatorname{Im} z = \operatorname{Im} w$ . It is useful, but most pairs, such as $1$ and $i$ , are incomparable — consistent with Theorem 6.)

ComputationC

Computing with complex numbers

Roots of unity and De Moivre's theoremPythonNumerical approximationSymbolic computationComputationally tested

"""Roots of unity, De Moivre's theorem and a square-root trap.

Numerically: the n numbers cos(2 pi k/n) + i sin(2 pi k/n) satisfy z^n = 1
up to rounding, add up to 0, multiply to (-1)^(n+1), and are spaced 2 sin(pi/n)
apart (a regular n-gon). Symbolically (SymPy): the exact cube roots of 1, and
the triple-angle formula cos 3t = 4 cos^3 t - 3 cos t read off from De
Moivre's theorem. Finally the trap: with principal square roots,
sqrt(-1) * sqrt(-1) = -1 while sqrt((-1) * (-1)) = 1.
"""

import cmath
import math

import sympy

def roots_of_unity(n):
    """The n complex numbers cis(2 pi k / n), k = 0, ..., n - 1."""
    if n < 1:
        raise ValueError("n must be at least 1")
    return [cmath.rect(1.0, 2 * math.pi * k / n) for k in range(n)]

def max_error_power(n):
    """max |z^n - 1| over the computed n-th roots of unity (rounding only)."""
    return max(abs(z ** n - 1) for z in roots_of_unity(n))

def root_sum(n):
    """Sum of the n-th roots of unity (exactly 0 for n >= 2)."""
    return sum(roots_of_unity(n))

def root_product(n):
    """Product of the n-th roots of unity (exactly (-1)^(n+1))."""
    product = 1
    for z in roots_of_unity(n):
        product *= z
    return product

def side_length(n):
    """Distance between neighbouring n-th roots of unity."""
    zs = roots_of_unity(n)
    return abs(zs[1 % n] - zs[0])

def exact_cube_roots():
    """The roots of z^3 - 1 as exact SymPy expressions, sorted by argument."""
    z = sympy.symbols("z")
    roots = sympy.solve(z ** 3 - 1, z)
    return sorted(roots, key=lambda r: float(sympy.arg(r)) % (2 * math.pi))

def triple_angle():
    """Real and imaginary parts of (cos t + i sin t)^3, in terms of cos, sin."""
    t = sympy.symbols("t", real=True)
    c, s = sympy.cos(t), sympy.sin(t)
    w = sympy.expand((c + sympy.I * s) ** 3)
    re_part = sympy.re(w).subs(s ** 2, 1 - c ** 2)
    im_part = sympy.im(w).subs(c ** 2, 1 - s ** 2)
    return sympy.expand(re_part), sympy.expand(im_part)

def main():
    print(" n  max|z^n - 1|  |sum|    |prod - (-1)^(n+1)|  side      2 sin(pi/n)")
    for n in range(3, 9):
        prod_err = abs(root_product(n) - (-1) ** (n + 1))
        print(
            f"{n:2d}  {max_error_power(n):.1e}      {abs(root_sum(n)):.1e}"
            f"  {prod_err:.1e}              {side_length(n):.6f}"
            f"  {2 * math.sin(math.pi / n):.6f}"
        )
    print("Errors of about 1e-15 are floating-point rounding, not mathematics.")
    print()
    roots = ", ".join(str(r) for r in exact_cube_roots())
    print(f"Exact cube roots of 1 (SymPy): {roots}")
    re_part, im_part = triple_angle()
    print("De Moivre, n = 3: (cos t + i sin t)^3 = cos 3t + i sin 3t, so")
    print(f"  cos 3t = {re_part}")
    print(f"  sin 3t = {im_part}")
    print()
    a = cmath.sqrt(-1) * cmath.sqrt(-1)
    b = cmath.sqrt((-1) * (-1))
    print(f"sqrt(-1) * sqrt(-1) = {a.real:+.0f}   but   sqrt((-1)(-1)) = {b.real:+.0f}")
    print("So sqrt(ab) = sqrt(a) sqrt(b) fails when a and b are negative.")
    print()
    print("Epistemic status: the table is numerical evidence for n = 3..8 only;")
    print("the lesson proves z^n = 1, the sum and the spacing for every n. The")
    print("SymPy results are exact symbolic computations, as trustworthy as")
    print("SymPy's algebra; De Moivre's theorem itself is proved by induction.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The tiny errors in the table, around $10^{-15}$ , come from rounding in floating-point arithmetic, not from the mathematics: Theorem 4 says the true errors are exactly $0$ . The table is evidence for six values of $n$ ; the theorem covers all of them.

Theorem 1 has a beautiful consequence for whole numbers. If $a, b, c, d$ are integers, the two-squares identity says that a product of two sums of two squares is again a sum of two squares — and complex multiplication tells you which squares:

Complex multiplication and sums of two squaresPythonExact computationExhaustive finite checkComputationally tested

"""Multiplying complex numbers multiplies sums of two squares.

For Gaussian integers z = a + bi (a, b whole numbers) the squared modulus
N(z) = a^2 + b^2 is a sum of two squares, and |zw|^2 = |z|^2 |w|^2 says that
(a^2 + b^2)(c^2 + d^2) = (ac - bd)^2 + (ad + bc)^2. The experiment checks this
exhaustively on a grid of Gaussian integers (exact integer arithmetic), then
uses complex multiplication to *produce* new sums of two squares, e.g.
65 = 5 * 13 = 1^2 + 8^2 = 4^2 + 7^2 from (1 + 2i)(2 + 3i) and (1 + 2i)(2 - 3i).
"""

import math

def gauss_mul(z, w):
    """Product of Gaussian integers given as pairs (a, b) meaning a + bi."""
    (a, b), (c, d) = z, w
    return (a * c - b * d, a * d + b * c)

def norm(z):
    """N(a + bi) = a^2 + b^2, the squared modulus."""
    a, b = z
    return a * a + b * b

def grid(radius):
    """All Gaussian integers a + bi with |a|, |b| <= radius."""
    if radius < 0:
        raise ValueError("radius must be non-negative")
    values = range(-radius, radius + 1)
    return [(a, b) for a in values for b in values]

def check_multiplicative(radius):
    """Return (pairs checked, failures) for N(zw) == N(z) N(w) on the grid."""
    points = grid(radius)
    failures = [
        (z, w)
        for z in points
        for w in points
        if norm(gauss_mul(z, w)) != norm(z) * norm(w)
    ]
    return len(points) ** 2, failures

def two_square_reps(n):
    """All (a, b) with 0 <= a <= b and a^2 + b^2 = n."""
    reps = []
    for a in range(math.isqrt(n // 2) + 1):
        b2 = n - a * a
        b = math.isqrt(b2)
        if b * b == b2 and a <= b:
            reps.append((a, b))
    return reps

def normalise(z):
    """Sort |real|, |imag| so a representation reads (small, large)."""
    a, b = abs(z[0]), abs(z[1])
    return (min(a, b), max(a, b))

def show(z):
    """Write the pair (a, b) as the text a + bi (or a - bi)."""
    a, b = z
    sign = "-" if b < 0 else "+"
    return f"{a} {sign} {abs(b)}i"

def square(x):
    """x^2 as text, with brackets around negative x."""
    return f"({x})^2" if x < 0 else f"{x}^2"

def main():
    cases, failures = check_multiplicative(6)
    print("N(zw) = N(z)N(w) for all z, w with coordinates in -6..6:")
    print(f"  {cases} pairs checked, {len(failures)} failures")
    print()
    z, w = (1, 2), (2, 3)
    w_bar = (2, -3)
    for v in (w, w_bar):
        p = gauss_mul(z, v)
        print(f"({show(z)})({show(v)}) = {show(p)},  "
              f"N = {square(p[0])} + {square(p[1])} = {norm(p)}")
    print("So 5 * 13 = 65 has two representations:", two_square_reps(65))
    print()
    print("n   = a^2 + b^2   (all representations with 0 <= a <= b)")
    for n in [5, 13, 25, 65, 85, 325, 1105]:
        reps = two_square_reps(n)
        shown = ", ".join(f"{a}^2+{b}^2" for a, b in reps)
        print(f"{n:<5} {shown}")
    print("3, 7, 21 have none:", [two_square_reps(n) for n in (3, 7, 21)])
    print()
    print("Epistemic status: the grid check is exhaustive but finite; the")
    print("identity (a^2+b^2)(c^2+d^2) = (ac-bd)^2+(ad+bc)^2 is proved for all")
    print("numbers by expanding both sides (and in Lean). Which n are sums of")
    print("two squares is a theorem of Fermat and Euler, not shown here.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Exercises

1. Complex numbers

Warm-upHuman

Compute $(4 - 3i)(2 + 5i)$ and enter its real part.

2. Complex numbers

Warm-upHuman

What is $i^{2027}$ ?

Choose one

-i

i

-1

1

3. Complex numbers

Warm-upHuman

Compute $\left|(3 + 4i)(5 - 12i)\right|$ — ideally without multiplying out first.

4. Complex numbers

CoreHuman

Which is the polar form of $z = -1 + i\sqrt 3$ ?

Choose one

2\operatorname{cis}\tfrac{2\pi}{3}

2\operatorname{cis}\left(-\tfrac{\pi}{3}\right)

4\operatorname{cis}\tfrac{2\pi}{3}

2\operatorname{cis}\tfrac{\pi}{3}

5. Complex numbers

CoreHuman

Solve $z^2 - 4z + 13 = 0$ .

Choose one

z = 2 \pm 3i

z = -2 \pm 3i

z = 2 \pm 6i

There are no solutions

6. Complex numbers

CoreHuman

Which of the following are sixth roots of unity, i.e. solutions of $z^6 = 1$ ? (Choose all that apply.)

Choose all that apply

7. Complex numbers

StretchHuman

What is wrong with this "proof" that $1 = -1$ ? $1 = \sqrt 1 = \sqrt{(-1)(-1)} = \sqrt{-1}\,\sqrt{-1} = i \cdot i = -1.$

Choose one

The step

\sqrt{(-1)(-1)} = \sqrt{-1}\,\sqrt{-1}

The step

1 = \sqrt 1

The step

i \cdot i = -1

The step

\sqrt 1 = \sqrt{(-1)(-1)}

8. Complex numbers

CoreFormal

In the Lean module, cis θ means $\cos\theta + i\sin\theta$ and n : ℕ. Which Lean statement is De Moivre's theorem?

Choose one

cis θ ^ n = cis (n * θ)cis (θ ^ n) = cis θ ^ ncis θ * n = cis (n * θ)cis (θ + n) = cis θ * cis n

9. Complex numbers

StretchComputational

Write nth_roots(w, n) that returns a list of the $n$ complex $n$ -th roots of a non-zero complex number w, using polar form: if $w = R\operatorname{cis}\varphi$ , the roots are $R^{1/n}\operatorname{cis}\frac{\varphi + 2\pi k}{n}$ for $k = 0, \dots, n-1$ . Python's cmath.polar(w) returns $(R, \varphi)$ and cmath.rect(r, theta) returns $r\operatorname{cis}\theta$ .

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"Imaginary numbers are fake." The word "imaginary" (Descartes' term, meant dismissively) is a historical accident. Complex numbers are as legitimate as negative numbers or $\sqrt 2$ : they can be constructed from real numbers (as pairs), they obey precise laws, and they describe real phenomena — alternating currents, waves, quantum amplitudes.

Misconception

" $\sqrt{ab} = \sqrt a\,\sqrt b$ always." It holds for $a, b \ge 0$ , but not for negative numbers: with $\sqrt{-1} = i$ , we get $\sqrt{-1}\cdot\sqrt{-1} = i^2 = -1$ , while $\sqrt{(-1)(-1)} = \sqrt 1 = 1$ . Every non-zero complex number has two square roots, and no choice of "the" square root can make the product rule work everywhere. Treat $\sqrt{-4}$ as $2i$ , and simplify before multiplying.

Misconception

" $\C$ can be ordered like $\R$ ." Theorem 6 shows no ordering is compatible with multiplication. Inequalities between complex numbers are meaningless; inequalities between their moduli, real parts or imaginary parts (all real numbers) are fine.

Misconception

" $|a + bi| = a + b$ " or " $|a + bi| = \sqrt{a^2 - b^2}$ ". The modulus is a distance in the plane: $|a + bi| = \sqrt{a^2 + b^2}$ . For example $|3 - 4i| = 5$ .

Misconception

"The argument is $\arctan\tfrac ba$ ." That gives an angle in $(-\tfrac\pi2, \tfrac\pi2)$ only, so it is wrong for points with $a < 0$ , and undefined when $a = 0$ . Always check the quadrant: $\arg(-1 - i) = -\tfrac{3\pi}{4}$ , not $\tfrac\pi4$ .

ViewpointsH

Other ways of seeing

Geometry— Similarities of the plane

Multiplication by $w \ne 0$ is a rotation by $\arg w$ combined with a scaling by $|w|$ , and $z \mapsto wz + c$ is a similarity of the plane fixing orientation; $z \mapsto \bar z$ is a reflection. Every rigid motion of the plane is $z \mapsto wz + c$ or $z \mapsto w\bar z + c$ with $|w| = 1$ . Geometry problems about rotations become algebra: for instance, $z_1, z_2, z_3$ form an equilateral triangle (or all coincide) exactly when $z_1 + \omega z_2 + \omega^2 z_3 = 0$ for $\omega = \operatorname{cis}\tfrac{2\pi}{3}$ or $\omega = \operatorname{cis}(-\tfrac{2\pi}{3})$ , the two choices corresponding to the two orientations.

Algebra— Adjoining a root

Algebraically, $\C$ is what you get by adjoining to $\R$ a root of $x^2 + 1$ : the quotient ring $\R[x]/(x^2 + 1)$ , where polynomials are computed modulo $x^2 + 1$ , so $x$ plays the role of $i$ . Conjugation $a + bi \mapsto a - bi$ respects addition and multiplication and fixes $\R$ — it is a field automorphism, and the two automorphisms of $\C$ fixing $\R$ form the first example of a Galois group. The matrices $\begin{pmatrix} a & -b \\ b & a\end{pmatrix}$ give yet another model of $\C$ , inside $2 \times 2$ real matrices. See Fields and Galois theory.

Number theory— Gaussian integers

The numbers $a + bi$ with $a, b \in \Z$ form the Gaussian integers $\Z[i]$ , where factorisation behaves differently: $5 = (2 + i)(2 - i)$ and $13 = (3 + 2i)(3 - 2i)$ , while $3$ cannot be split. Since $N(z) = |z|^2 = a^2 + b^2$ is multiplicative (Theorem 1), a prime $p$ factors in $\Z[i]$ exactly when $p = a^2 + b^2$ for some integers $a, b$ . Fermat's theorem that odd primes of the form $4k + 1$ are sums of two squares (proved by Euler) is the starting point of algebraic number theory.

Topology— Why every polynomial has a root: a winding argument

Here is the idea of one proof of the fundamental theorem of algebra — a sketch, not a proof. Let $p(z) = z^n + a_{n-1}z^{n-1} + \dots + a_0$ with $n \ge 1$ , and suppose $p$ had no root. For a huge circle $|z| = R$ , the term $z^n$ dominates, so as $z$ goes once around the circle, $p(z)$ winds $n$ times around $0$ . Now shrink the circle continuously to the point $0$ : the image curve deforms continuously, never passing through $0$ (no roots!), so its winding number cannot jump — yet at the end the curve is the single point $p(0) \ne 0$ , which winds $0$ times. Since $n \ne 0$ , contradiction. Making "winding number" and "cannot jump" precise is a job for the fundamental group or complex analysis.

Counting how often a curve winds around a point

How many times does the curve wind around the point p? Count the turns of an arrow, or the signed crossings of a ray.

Curve

winding number 1

Drag the points, or focus one with Tab and use the arrow keys (hold Shift for small steps).

Move along the curve0.17 turns so far

p =Re+Imi

Winding number around p: 1

By the angle: as the gold point goes once around the curve, the arrow from p turns 1 full turns (counter-clockwise counts as positive).

By the ray: signed crossings (+1) = 1

Each crossing of the dashed ray counts +1 where the curve passes upwards (counter-clockwise around p) and −1 where it passes downwards (clockwise).

Both counts are computed on the curve sampled at 720 points.

Physics— Rotating arrows for waves

An alternating voltage $V_0\cos(\omega t + \varphi)$ is the real part of the rotating complex number $V_0 \operatorname{cis}(\omega t + \varphi)$ (a "phasor"). Adding waves of the same frequency becomes adding complex numbers, and the effect of a capacitor or inductor becomes multiplication by a complex impedance. In quantum mechanics complex numbers are not a convenience but part of the theory: states are described by complex amplitudes whose squared moduli give probabilities.

Wonder Trails

Optional, and never graded: a question that leads somewhere further.

Wonder Trail · Optional · never gradedLoops around a holeWalk around a tree and come back to where you started. How many times did you go around it? Can you change that number by wandering differently — without ever walking through the tree?Follow the trail

History & global context

History and global context

Early encounters. Heron of Alexandria (1st century CE) met the square root of a negative number in a calculation about a truncated pyramid and passed over it. The Indian mathematician Mahāvīra (9th century) stated that a negative number has no square root, since it is not a square.
Renaissance Italy. Gerolamo Cardano's Ars Magna (1545) contains the cubic formula and, in another problem, the "sophisticated" numbers $5 \pm \sqrt{-15}$ , which have sum $10$ and product $40$ . Rafael Bombelli's Algebra (1572) gave the first systematic rules for calculating with them, motivated by $x^3 = 15x + 4$ .
Names and symbols. René Descartes called such roots "imaginary" in La Géométrie (1637). Abraham de Moivre found formulas equivalent to his theorem in the early 18th century; Leonhard Euler stated $e^{i\theta} = \cos\theta + i\sin\theta$ in his Introductio (1748) and introduced the symbol $i$ (1777).
The plane. The surveyor Caspar Wessel (1799, in Danish), Jean-Robert Argand (1806) and Carl Friedrich Gauss (1831) described complex numbers as points of a plane. Gauss's doctoral thesis (1799) was devoted to the fundamental theorem of algebra; its proof was later seen to leave a topological point unproved, and Gauss gave further proofs. William Rowan Hamilton defined complex numbers as pairs of reals (1837).

A square root that would not go away

Numbers you can turn

Definitions

Worked examples

Explore: arithmetic as geometry

Theorems and proofs

Complex numbers in Lean

Computing with complex numbers

Exercises

Common misconceptions

Other ways of seeing

Wonder Trails

History and global context

Further reading