WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Euclidean space

Revision #3166 → #3667 · back to history

modifiedRiemannian manifold1b87ef1af50c
FieldFrom #3166To #3667
mathlib.declContMDiffRiemannianMetricIsContMDiffRiemannianBundle
noteMathlib has `ContMDiffRiemannianMetric` and `IsContMDiffRiemannianBundle` for Riemannian metrics on the tangent bundle, but no top-level `RiemannianManifold` structure.Mathlib has `IsContMDiffRiemannianBundle` for Riemannian metrics on the tangent bundle, but no top-level `RiemannianManifold` structure.
addedAffine space over a field5f6b6545dc21
addedProjective space37e1c66d7644
addedGreat circle / orthodrome9debd83faff7
addedParallel postulatedc76d6154faf
addedTangent space of a manifold5a90944884f2