OAI/Geometry/EinsteinFour/HighestLinear.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

The exact linear equations and their elementary eliminations.

  1. structure OAI.PositiveEinsteinFour.HighestHessian.Equations line 15

    Source documentation

    These are precisely the independent scalar trace and Bianchi equations.

    structure Equations (c : Fin 50 → ℝ) : Prop where
…
  2. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_0 line 46
  3. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_1 line 51
  4. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_2 line 56
  5. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_3 line 61
  6. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_4 line 66
  7. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_5 line 71
  8. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_6 line 76
  9. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_7 line 81
  10. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_8 line 86
  11. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_9 line 91
  12. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_10 line 96
  13. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_11 line 101
  14. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_12 line 106
  15. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_13 line 111
  16. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_14 line 116
  17. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_15 line 121
  18. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_16 line 126
  19. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_17 line 131
  20. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_18 line 136
  21. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_19 line 141
  22. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_20 line 146
  23. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_22 line 151
  24. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_23 line 156
  25. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_25 line 161
  26. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_27 line 166
  27. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_28 line 171
  28. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_30 line 176
  29. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_32 line 181
  30. theorem OAI.PositiveEinsteinFour.HighestHessian.Equations.pivot_33 line 186