Map · 32
several complex variables
MSC 32 · Several complex variables and analytic spaces
668 declarations (625 theorems, 43 definitions) across 11 files. 1 of the 11 famous theorems listed for this area are in Mathlib (9%). 1 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.
Subareas2
- 32A Holomorphic functions of several complex variables 628
- 32Q Complex manifolds 40
Famous theorems1 of 11
From the 1000+ theorems project, which classifies each theorem by MSC area.
Not yet in Mathlib · 10
In Mathlib · 1
- Weierstrass preparation theoremPowerSeries.exists_isWeierstrassFactorization
Open conjectures stated in Lean1
Statements without proofs, collected by the Formal Conjectures project.
- Erdos1041.erdos_1041Erdős Problems
Files11
Largest first. The code after each file is its assigned subarea.
- Mathlib.Analysis.Analytic.Constructions
Various ways to combine analytic functions
32A · 211
- Mathlib.Analysis.Analytic.Basic
Analytic functions
32A · 140
- Mathlib.Analysis.Analytic.Composition
Composition of analytic functions
32A · 80
- Mathlib.Analysis.Analytic.CPolynomialDef
We specialize the theory of analytic functions to the case of functions that admit a development given by a *finite* for
32A · 64
- Mathlib.Analysis.Analytic.CPolynomial
Properties of continuously polynomial functions
32A · 42
- Mathlib.Analysis.Analytic.ChangeOrigin
Changing origin in a power series
32A · 41
- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Manifold structure on the upper half plane.
32Q · 33
- Mathlib.MeasureTheory.Integral.TorusIntegral
Integral over a torus in `ℂⁿ`
32A · 24
- Mathlib.Analysis.Analytic.Inverse
Inverse of analytic functions
32A · 23
- Mathlib.Geometry.Manifold.Complex
Holomorphic functions on complex manifolds
32Q · 7
- Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
Analyticity of local inverses
32A · 3