OAI/LinearAlgebra/MatrixMultiplication/Tensor/ComplexTensorSymmetrization.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. def OAI.MatrixMultiplication.Foundation.Tensor.cyclic line 14
  2. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.cyclic line 17
  3. def OAI.MatrixMultiplication.Foundation.Tensor.directSumProductEquiv line 27
  4. theorem OAI.MatrixMultiplication.Foundation.Tensor.directSum_product line 34
  5. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.directSum_product line 65
  6. theorem OAI.MatrixMultiplication.Foundation.Tensor.directSum_pullback line 74
  7. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.directSum_pullback line 80
  8. theorem OAI.MatrixMultiplication.Foundation.Tensor.cyclic_directSum line 87
  9. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.directSum_cyclic line 105
  10. def OAI.MatrixMultiplication.Foundation.Tensor.directSumPowerEquiv line 111
  11. theorem OAI.MatrixMultiplication.Foundation.Tensor.directSum_power line 118
  12. theorem OAI.MatrixMultiplication.Foundation.Tensor.directSum_const_power line 131
  13. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.directSum_const_of_power line 138
  14. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.directSum_const_power line 147
  15. def OAI.MatrixMultiplication.Foundation.Tensor.rectangularSquareX line 156
  16. def OAI.MatrixMultiplication.Foundation.Tensor.rectangularSquareY line 163
  17. def OAI.MatrixMultiplication.Foundation.Tensor.rectangularSquareZ line 170
  18. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_directSum_rank_of_power line 179
  19. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_cyclic_product_square line 199
  20. theorem OAI.MatrixMultiplication.Foundation.Tensor.cyclic_matrixCoefficients line 231
  21. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_symmetrized_rank line 236
  22. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_directSum_symmetrized_rank line 246
  23. theorem OAI.MatrixMultiplication.Foundation.Tensor.symmetrized_tag_card line 259
  24. theorem OAI.MatrixMultiplication.Foundation.Tensor.symmetrized_index_card line 264