OAI/Geometry/EinsteinFour/CurvatureFirstBianchi.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The first Bianchi identity follows directly from the symmetric Levi-Civita Christoffel symbols and is preserved by frame contraction.

  1. theorem OAI.PositiveEinsteinFour.Geometry.metricInChart_comm line 18
  2. theorem OAI.PositiveEinsteinFour.Geometry.christoffel_comm line 22
  3. theorem OAI.PositiveEinsteinFour.Geometry.curvatureComponent_first_bianchi line 33
  4. theorem OAI.PositiveEinsteinFour.Geometry.sum_three_cycle line 59
  5. theorem OAI.PositiveEinsteinFour.Geometry.contracted_bianchi line 68
  6. theorem OAI.PositiveEinsteinFour.Geometry.frameCurvature_first_bianchi line 105