OAI/Algebra/FiniteTensor/FormReindexing.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Exterior reindexing, separated potentials and parity of Koszul operators.

  1. def OAI.PD4Tensor.Forms.coordinateIsometry line 17
  2. def OAI.PD4Tensor.Forms.reindexExterior line 22
  3. theorem OAI.PD4Tensor.Forms.reindexExterior_ι line 25
  4. theorem OAI.PD4Tensor.Forms.reindexExterior_dx line 32
  5. theorem OAI.PD4Tensor.Forms.reindexExterior_parity line 41
  6. def OAI.PD4Tensor.Forms.reindexForms line 51
  7. theorem OAI.PD4Tensor.Forms.reindexForms_tmul line 54
  8. theorem OAI.PD4Tensor.Forms.reindexForms_scalar line 57
  9. theorem OAI.PD4Tensor.Forms.reindexForms_differential line 61
  10. theorem OAI.PD4Tensor.Forms.reindexForms_parity line 73
  11. def OAI.PD4Tensor.FrobeniusTruncation.coordinateEquiv line 87
  12. theorem OAI.PD4Tensor.FrobeniusTruncation.coordinateEquiv_coord line 92
  13. theorem OAI.PD4Tensor.FrobeniusTruncation.coordinateEquiv_derivative line 97
  14. def OAI.PD4Tensor.TruncatedForms.sigmaHeadTail line 111
  15. def OAI.PD4Tensor.TruncatedForms.blockSigmaEquiv line 120
  16. theorem OAI.PD4Tensor.TruncatedForms.blockSigmaEquiv_zero line 134
  17. theorem OAI.PD4Tensor.TruncatedForms.blockSigmaEquiv_inl line 136
  18. theorem OAI.PD4Tensor.TruncatedForms.blockSigmaEquiv_inr line 138
  19. def OAI.PD4Tensor.TruncatedForms.sigmaSeparatedEquiv line 148
  20. theorem OAI.PD4Tensor.TruncatedForms.D_sigmaSeparated line 157
  21. theorem OAI.PD4Tensor.FrobeniusTruncation.rename_rename line 176
  22. theorem OAI.PD4Tensor.FrobeniusTruncation.coordinateEquiv_eq_rename line 184
  23. def OAI.PD4Tensor.TruncatedForms.sigmaPotential line 198
  24. def OAI.PD4Tensor.TruncatedForms.sigmaProduct line 204
  25. theorem OAI.PD4Tensor.TruncatedForms.separatedPotential_reindex line 209
  26. theorem OAI.PD4Tensor.TruncatedForms.separatedProduct_reindex line 235
  27. theorem OAI.PD4Tensor.TruncatedForms.reindex_koszul line 263
  28. theorem OAI.PD4Tensor.TruncatedForms.reindex_mulScalar line 275
  29. theorem OAI.PD4Tensor.TruncatedForms.koszul_sigmaSeparated line 283
  30. theorem OAI.PD4Tensor.TruncatedForms.mulScalar_sigmaSeparated line 300
  31. theorem OAI.PD4Tensor.TruncatedForms.koszul_parity line 324
  32. theorem OAI.PD4Tensor.TruncatedForms.mulScalar_parity line 332
  33. theorem OAI.PD4Tensor.TruncatedForms.koszul_zero line 339
  34. theorem OAI.PD4Tensor.TruncatedForms.mulScalar_one line 346
  35. theorem OAI.PD4Tensor.oddCoordinate_congr_at line 362
  36. theorem OAI.PD4Tensor.oddTensor_single line 370