OAI/Geometry/EinsteinFour/MetricContractionCalculus.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Differentiate contraction by the actual inverse metric. This is the local identity needed to commute covariant differentiation with trace.

  1. theorem OAI.PositiveEinsteinFour.Geometry.partialDeriv_matrix_trace line 15
  2. theorem OAI.PositiveEinsteinFour.Geometry.metric_trace_derivative_algebra line 24
  3. theorem OAI.PositiveEinsteinFour.Geometry.partialDeriv_metric_contraction line 38