OAI/Algebra/FiniteTensor/OddTensors.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Odd coordinate operators, tensor signs and naturality.

  1. def OAI.PD4Tensor.oddCoordinate line 17
  2. def OAI.PD4Tensor.oddTensor line 20
  3. theorem OAI.PD4Tensor.tprod_neg_at line 25
  4. theorem OAI.PD4Tensor.odd_term_lt line 36
  5. theorem OAI.PD4Tensor.odd_term_anticommute line 54
  6. theorem OAI.PD4Tensor.oddTensor_anticommute line 78
  7. theorem OAI.PD4Tensor.tensorMap_oddTensor_zero line 95
  8. theorem OAI.PD4Tensor.oddTensor_tensorMap_zero line 109
  9. theorem OAI.PD4Tensor.oddTensor_sandwich line 123
  10. theorem OAI.PD4Tensor.oddTensor_naturality line 143
  11. theorem OAI.PD4Tensor.headTail_map line 171
  12. theorem OAI.PD4Tensor.headTail_oddTensor line 181