OAI/LinearAlgebra/MatrixMultiplication/Tensor/TensorSidePermutation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. def OAI.MatrixMultiplication.Foundation.Tensor.sidePermutation line 14
  2. theorem OAI.MatrixMultiplication.Foundation.Tensor.coordinates_eta line 19
  3. theorem OAI.MatrixMultiplication.Foundation.Tensor.sidePermutation_apply_coordinates line 23
  4. theorem OAI.MatrixMultiplication.Foundation.Tensor.sidePermutation_refl line 29
  5. theorem OAI.MatrixMultiplication.Foundation.Tensor.sidePermutation_symm line 33
  6. theorem OAI.MatrixMultiplication.Foundation.Tensor.sidePermutation_apply_symm line 45
  7. def OAI.MatrixMultiplication.Foundation.Tensor.coordinatesEquiv line 50
  8. def OAI.MatrixMultiplication.Foundation.Tensor.permuteCoordinates line 56
  9. theorem OAI.MatrixMultiplication.Foundation.Tensor.restrict_eq_sum_coordinates line 65
  10. theorem OAI.MatrixMultiplication.Foundation.Tensor.restrict_sidePermutation line 76
  11. def OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.sidePermutation line 111
  12. def OAI.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.restoreSides line 121