Map · 53
differential geometry
MSC 53 · Differential geometry
148 declarations (104 theorems, 44 definitions) across 8 files. 0 of the 37 famous theorems listed for this area are in Mathlib (0%), 1 in some Lean library.
Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.
Subareas2
- 53C Global differential geometry 124
- 53A Classical differential geometry 24
Famous theorems0 of 37
From the 1000+ theorems project, which classifies each theorem by MSC area.
Structures defined here3
Typeclasses defined in this area's files, most assumed first.
Files8
Largest first. The code after each file is its assigned subarea.
- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
Covariant derivatives
53C · 55
- Mathlib.Geometry.Manifold.Riemannian.Basic
Riemannian manifolds
53C · 28
- Mathlib.Geometry.Manifold.Riemannian.PathELength
Lengths of paths in manifolds
53C · 21
- Mathlib.Analysis.Calculus.Conformal.NormedSpace
Conformal Maps
53A · 16
- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
Torsion of an affine connection
53C · 12
- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
Metric connections
53C · 8
- Mathlib.Analysis.Calculus.Conformal.InnerProduct
Conformal maps between inner product spaces
53A · 6
- Mathlib.Geometry.Manifold.ConformalGroupoid
Conformal Groupoid
53A · 2