OAI/Geometry/EinsteinFour/MetricInverseCalculus.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The inverse metric is parallel. Its coordinate derivative is derived from the inverse identity and the proved metric compatibility equation.

  1. theorem OAI.PositiveEinsteinFour.Geometry.inverse_metric_derivative_algebra line 16
  2. theorem OAI.PositiveEinsteinFour.Geometry.matrixPartial_inverseMetric line 35