OAI/Analysis/JiangSu/TensorProducts/TensorSliceSeparation.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TensorSliceSeparation.slice line 16
  2. lemma OAI.TensorSliceSeparation.slice_tmul line 19
  3. lemma OAI.TensorSliceSeparation.tensor_eq_zero_of_slices line 22
  4. lemma OAI.TensorSliceSeparation.tensor_eq_zero_of_double_slices line 46
  5. abbrev OAI.MatrixTensor.Mat line 65
  6. def OAI.MatrixTensor.left line 67
  7. def OAI.MatrixTensor.right line 88
  8. lemma OAI.MatrixTensor.left_mul_right line 109
  9. lemma OAI.MatrixTensor.right_mul_left line 119
  10. lemma OAI.MatrixTensor.commute line 129
  11. lemma OAI.MatrixTensor.left_mul_right_apply line 133
  12. instance OAI.MatrixTensor.matFiniteDimensional line 152
  13. instance OAI.MatrixTensor.closedSectionCStar line 156
  14. def OAI.MatrixTensor.leftSection line 162
  15. def OAI.MatrixTensor.rightSection line 172
  16. lemma OAI.MatrixTensor.section_commute line 183
  17. def OAI.MatrixTensor.sectionMap line 196
  18. lemma OAI.MatrixTensor.sectionMap_tmul line 201
  19. lemma OAI.MatrixTensor.sectionMap_tmul_entry line 204
  20. def OAI.MatrixTensor.entryLinear line 208
  21. lemma OAI.MatrixTensor.entryLinear_separates line 213
  22. lemma OAI.MatrixTensor.sectionMap_slice_entry line 220
  23. theorem OAI.MatrixTensor.sectionMap_injective line 229