4. Main theorems🔗

The main theorems of the library: first two stated in Mathlib's language, then two strands, algebraic schemes over a field of characteristic zero and real- and complex-analytic manifolds and spaces. Each section presents one theorem: the properties it asserts and the inputs particular to it, then the theorem and a sketch of its proof.

1. 4.1. Resolution of singularities in Mathlib's language
   1. 4.1.1. Resolution of a variety
   2. 4.1.2. Local monomialization of a real-analytic function
2. 4.2. Algebraic schemes
   1. 4.2.1. Main Theorem II: order reduction
   2. 4.2.2. Main Theorem II(N): principalization
   3. 4.2.3. Corollary 1: trivialization of a system of ideal sheaves
   4. 4.2.4. Functorial principalization
   5. 4.2.5. Corollary 3: simplification of a boundary
   6. 4.2.6. Functorial resolution
   7. 4.2.7. Strong resolution of a variety
   8. 4.2.8. Main Theorem I
   9. 4.2.9. Main Theorem I, weak form
   10. 4.2.10. Embedded desingularization with smooth centres
3. 4.3. Analytic manifolds and analytic spaces
   1. 4.3.1. Main Theorem II″(N), compatible-family form
   2. 4.3.2. Real-analytic principalization with the Jacobian condition
   3. 4.3.3. Functorial principalization on analytic manifolds
   4. 4.3.4. Embedded desingularization of analytic spaces
   5. 4.3.5. Resolution of analytic spaces
   6. 4.3.6. Resolution of a reduced complex-analytic space