The complex plane

Use two real coordinates for a complex number; take the points above the real axis.

Start with a concrete example

A number such as 2+3i has two coordinates: 2 across and 3 up. Its partner 2−3i sits below. A picture with two axes helps keep track of numbers with a real and an imaginary part.

A small check: try the idea

Think with the concrete example above. You can try again.

Which number lies above the horizontal real axis?

Read the answer and reasoning

2+3i. The imaginary coordinate gives vertical position: +3 is up, −3 is down.

Build the idea in three steps

Real numbers include integers, fractions and numbers such as √2; they give coordinates on a line. A complex number x + yi gives two real coordinates.
The imaginary unit i satisfies i² = −1. Think of x + yi as the point (x,y).
The upper half-plane is the region y > 0. Modular forms in these definitions take their inputs from that region.

A small example

2 + 3i is above the real axis; 2 − 3i is below. Only the first is an input in ℍ.

Use in Lean · original excerpt

FLT · aa2d8b3 · Def_FLTPrelim_Modularity.lean

19def qCoeff (f : ℍ → ℂ) (n : ℕ) : ℂ :=20  (qExpansion 1 f).coeff n

How to read this Lean

ℍ is the upper half-plane; ℂ is the complex numbers. This is an occurrence of those types, not their library definitions.

Original source ↗ · L19–20 Open the complete saved source

Where this idea is used

8. The secret duet 9. Two doors to the concert 10. A three-note audition 11. Borrow a better passport 12. The workshops agree 13. Pip’s impossible quilt 14. The shrinking reservation 15. The concert of absolute silence 16. The room with no room

The complex plane

Start with a concrete example

A small check: try the idea

Build the idea in three steps

A small example

Use in Lean · original excerpt

How to read this Lean

Where this idea is used

Mika’s help desk

One thing at a time

In simpler words

A small clue