Mathlib Map

Map · 30

complex analysis

MSC 30 · Functions of a complex variable

2,750 declarations (2,582 theorems, 168 definitions) across 87 files. 12 of the 62 famous theorems listed for this area are in Mathlib (19%), 15 in some Lean library. 15 open conjectures here are stated in Lean.

Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.

Subareas5

  • 30A General properties of functions of one complex variable 1,283
  • 30D Entire and meromorphic functions of one complex variable, and related topics 712
  • 30C Geometric function theory 387
  • 30B Series expansions of functions of one complex variable 207
  • 30E Miscellaneous topics of analysis in the complex plane 161

Famous theorems12 of 62

From the 1000+ theorems project, which classifies each theorem by MSC area.

Not yet in Mathlib · 50

In Mathlib · 12

From the 100 theorems list2

Open conjectures stated in Lean15

Statements without proofs, collected by the Formal Conjectures project.

Undergraduate topics still missing12 of 28

From Mathlib's own undergraduate checklist.

Single Variable Complex Analysis · 12 of 28

  • Complex-valued series › antiderivative
  • Functions on one complex variable › Cauchy-Riemann conditions
  • Functions on one complex variable › contour integrals of continuous functions in $\C$
  • Functions on one complex variable › antiderivatives of a holomorphic function
  • Functions on one complex variable › representations of the $\log$ function on $\C$
  • Functions on one complex variable › theorem of holomorphic functions under integral domains
  • Functions on one complex variable › winding number of a closed curve in $\C$ with respect to a point
  • Functions on one complex variable › isolated singularities
  • Functions on one complex variable › Laurent series
  • Functions on one complex variable › meromorphic functions
  • Functions on one complex variable › residue theorem
  • Functions on one complex variable › sequences and series of holomorphic functions

Files87

Largest first. The code after each file is its assigned subarea.