IndisputableMonolith.Relativity.Geometry
IndisputableMonolith/Relativity/Geometry.lean · 16 lines · 0 declarations
show as:
view math explainer →
1import IndisputableMonolith.Relativity.Geometry.Manifold
2import IndisputableMonolith.Relativity.Geometry.Tensor
3import IndisputableMonolith.Relativity.Geometry.Metric
4import IndisputableMonolith.Relativity.Geometry.Connection
5import IndisputableMonolith.Relativity.Geometry.Curvature
6import IndisputableMonolith.Relativity.Geometry.MetricUnification
7import IndisputableMonolith.Relativity.Geometry.LeviCivitaTheorem
8import IndisputableMonolith.Relativity.Geometry.ParallelTransport
9import IndisputableMonolith.Relativity.Geometry.DiscreteBridge
10
11/-!
12# Geometry Module Aggregator
13
14This module re-exports all geometry components for convenient importing.
15-/
16