OAI/LinearAlgebra/MatrixFields/Histories/CWShapePhysicalPermutation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.sidePermutation line 16
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.coordinates_eta line 21
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.sidePermutation_apply_coordinates line 25
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.sidePermutation_refl line 31
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.sidePermutation_symm line 35
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.sidePermutation_apply_symm line 47
  7. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.coordinatesEquiv line 52
  8. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.permuteCoordinates line 58
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.restrict_eq_sum_coordinates line 67
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.restrict_sidePermutation line 78
  11. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.sidePermutation line 113
  12. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.restoreSides line 123
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.CWShapePhysicalPermutation.tensor_swapXY_inline_MatrixMultiplication_CWShapePhysicalPermutation line 154
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.CWShapePhysicalPermutation.tensor_swapYZ_inline_MatrixMultiplication_CWShapePhysicalPermutation line 160
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.CWShapePhysicalPermutation.tensor_swapXZ_inline_MatrixMultiplication_CWShapePhysicalPermutation line 165
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.CWShapePhysicalPermutation.tensor_permute line 169
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.CWShapePhysicalPermutation.strand_permute line 187
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.CWShapePhysicalPermutation.shapeTensor_permute line 195
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.CWShapePhysicalPermutation.shapeTensor_prod_permute line 216
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.CWShapePhysicalPermutation.shapeTensor_prod_permute_ne_zero_iff line 227
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.CWShapePhysicalPermutation.sidePermutation_shapeTensor line 236