OAI/Algebra/FiniteTensor/TensorCoordinates.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Frobenius coordinate sums, tensor decompositions and exterior coordinate maps.

  1. def OAI.PD4Tensor.FrobeniusTruncation.evaluate line 18
  2. theorem OAI.PD4Tensor.FrobeniusTruncation.evaluate_coord line 25
  3. theorem OAI.PD4Tensor.FrobeniusTruncation.hom_ext line 30
  4. def OAI.PD4Tensor.FrobeniusTruncation.rename line 39
  5. theorem OAI.PD4Tensor.FrobeniusTruncation.rename_coord line 42
  6. def OAI.PD4Tensor.FrobeniusTruncation.toTensor line 46
  7. def OAI.PD4Tensor.FrobeniusTruncation.fromTensor line 57
  8. theorem OAI.PD4Tensor.FrobeniusTruncation.toTensor_inl line 61
  9. theorem OAI.PD4Tensor.FrobeniusTruncation.toTensor_inr line 64
  10. theorem OAI.PD4Tensor.FrobeniusTruncation.fromTensor_tmul line 67
  11. theorem OAI.PD4Tensor.FrobeniusTruncation.from_toTensor line 71
  12. theorem OAI.PD4Tensor.FrobeniusTruncation.to_fromTensor line 76
  13. def OAI.PD4Tensor.FrobeniusTruncation.sumTensorEquiv line 90
  14. theorem OAI.PD4Tensor.FrobeniusTruncation.rename_mk line 105
  15. theorem OAI.PD4Tensor.FrobeniusTruncation.derivative_rename line 117
  16. theorem OAI.PD4Tensor.FrobeniusTruncation.derivative_rename_other line 123
  17. def OAI.PD4Tensor.Forms.sumCoordinateIsometry line 146
  18. def OAI.PD4Tensor.Forms.sumExteriorEquiv line 154
  19. def OAI.PD4Tensor.Forms.inlCoordinate line 161
  20. def OAI.PD4Tensor.Forms.inrCoordinate line 164
  21. def OAI.PD4Tensor.Forms.inlExterior line 168
  22. def OAI.PD4Tensor.Forms.inrExterior line 169
  23. theorem OAI.PD4Tensor.Forms.sumExteriorEquiv_symm_tmul line 171
  24. theorem OAI.PD4Tensor.Forms.inlExterior_dx line 208
  25. theorem OAI.PD4Tensor.Forms.inrExterior_dx line 214
  26. theorem OAI.PD4Tensor.Forms.involute_map line 221