OAI/LinearAlgebra/MatrixMultiplication/Tensor/CompleteWordPair.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. structure OAI.MatrixMultiplication.PermutationMatching.CompleteWordPair line 14
  2. abbrev OAI.MatrixMultiplication.PermutationMatching.HalfClassPermutations line 18
  3. instance OAI.MatrixMultiplication.PermutationMatching.completeWordPairMulAction line 21
  4. theorem OAI.MatrixMultiplication.PermutationMatching.smul_completeWordPair_left line 29
  5. theorem OAI.MatrixMultiplication.PermutationMatching.smul_completeWordPair_right line 33