OAI/Geometry/EinsteinFour/HighestVectorSpace.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Linearity of the concrete highest-Hessian coordinates.

  1. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_add_0 line 14
  2. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_add_1 line 21
  3. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_add_2 line 28
  4. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_add_3 line 35
  5. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_add_4 line 42
  6. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_add_5 line 49
  7. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_add_6 line 56
  8. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_add_7 line 63
  9. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_add_8 line 70
  10. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_add_9 line 77
  11. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_smul_0 line 84
  12. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_smul_1 line 91
  13. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_smul_2 line 98
  14. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_smul_3 line 105
  15. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_smul_4 line 112
  16. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_smul_5 line 119
  17. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_smul_6 line 126
  18. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_smul_7 line 133
  19. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_smul_8 line 140
  20. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_smul_9 line 147
  21. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_add line 154
  22. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_smul line 168
  23. theorem OAI.PositiveEinsteinFour.HighestHessian.symmetricArray_add line 182
  24. theorem OAI.PositiveEinsteinFour.HighestHessian.symmetricArray_smul line 187
  25. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_add line 192
  26. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_smul line 196