Revision #1541 → #1791 · back to history
modifiedRiemann surface (lead)f3859a78371d
| Field | From #1541 | To #1791 |
|---|
| mathlib.match_kind | — | generalization |
addedSurfaces admitting / not admitting complex structures44f3fc44e31e
modifiedRiemann surface as complex manifold of dimension onede909d9999cc
| Field | From #1541 | To #1791 |
|---|
| mathlib.match_kind | — | generalization |
modifiedComplex structure induces conformal structure872e617e2d24
| Field | From #1541 | To #1791 |
|---|
| mathlib.match_kind | — | special_case |
modifiedComplex plane7078c8a9b0e9
| Field | From #1541 | To #1791 |
|---|
| mathlib.match_kind | — | generalization |
modifiedOpen subset of complex plane05b5d8d2a01d
| Field | From #1541 | To #1791 |
|---|
| mathlib.decl | TopologicalSpace.Opens.instIsManifold | TopologicalSpace.Opens.instIsManifoldSubtypeMem |
| mathlib.match_kind | — | generalization |
| note | Open subsets of a manifold (hence of ℂ) inherit a manifold structure, but not framed as Riemann surfaces. | Open subsets of a manifold (hence of ℂ) inherit a manifold structure via Opens.instIsManifoldSubtypeMem, but not framed as Riemann surfaces. |
modifiedOpen subset of a Riemann surface0b4918638420
| Field | From #1541 | To #1791 |
|---|
| mathlib.decl | TopologicalSpace.Opens.instIsManifold | TopologicalSpace.Opens.instIsManifoldSubtypeMem |
| mathlib.match_kind | — | generalization |
| note | Mathlib's instance gives that any open subset (Opens M) of a manifold is again a manifold, generalizing the Riemann-surface case. | Mathlib's Opens.instIsManifoldSubtypeMem gives that any open subset of a manifold is again a manifold, generalizing the Riemann-surface case. |
addedRiemann sphere as projective line48bcb87f2a8b
modifiedEvery elliptic curve is an algebraic curveb6963c778b42
| Field | From #1541 | To #1791 |
|---|
| mathlib.match_kind | — | generalization |
modifiedHolomorphic map between Riemann surfacesd7efe5f64230
| Field | From #1541 | To #1791 |
|---|
| mathlib.match_kind | — | generalization |
| mathlib.module | Mathlib.Geometry.Manifold.MFDeriv.Basic | Mathlib.Geometry.Manifold.MFDeriv.Defs |
modifiedBiholomorphic / conformally equivalent surfacesbf08c07f7340
| Field | From #1541 | To #1791 |
|---|
| mathlib.match_kind | — | generalization |
addedJacobian determinant of complex multiplication is |a|²f0cb395bc3ed
addedKodaira embedding for compact Riemann surfacesf2386d1df685
modifiedTorus, Weierstrass function and elliptic curve5d0d5af272a0
| Field | From #1541 | To #1791 |
|---|
| mathlib.match_kind | — | special_case |
addedTeichmüller space and moduli (parabolic)c7d0e87afc86
modifiedLiouville and Little Picard constancy5e4200ca1536
| Field | From #1541 | To #1791 |
|---|
| mathlib.match_kind | — | special_case |
addedRiemann–Hurwitz formula8129e399a44f
addedSimple group of order 168 is second-smallest non-abelian simple1cdee73c2f8c
addedRiemann–Roch theorem (listed)626f9f89f534
addedIdentity theorem for Riemann surfaces (listed)073069a2ec1b