OAI/LinearAlgebra/MatrixMultiplication/Tensor/ComplexTensor.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. abbrev OAI.MatrixMultiplication.Foundation.Tensor line 16
  2. def OAI.MatrixMultiplication.Foundation.Tensor.rankOne line 24
  3. def OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost line 27
  4. def OAI.MatrixMultiplication.Foundation.Tensor.restrict line 31
  5. def OAI.MatrixMultiplication.Foundation.Tensor.contract line 37
  6. def OAI.MatrixMultiplication.Foundation.Tensor.product line 41
  7. def OAI.MatrixMultiplication.Foundation.Tensor.directSum line 45
  8. def OAI.MatrixMultiplication.Foundation.Tensor.power line 49
  9. theorem OAI.MatrixMultiplication.Foundation.Tensor.directSum_matching line 53
  10. theorem OAI.MatrixMultiplication.Foundation.Tensor.directSum_zero_of_left_ne line 58
  11. theorem OAI.MatrixMultiplication.Foundation.Tensor.rankAtMost_zero line 63
  12. theorem OAI.MatrixMultiplication.Foundation.Tensor.rankOne_rankAtMost line 68
  13. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.map line 74
  14. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.scale line 82
  15. theorem OAI.MatrixMultiplication.Foundation.Tensor.rankAtMost_sum_rankOne line 90
  16. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.product line 102
  17. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.power line 126
  18. theorem OAI.MatrixMultiplication.Foundation.Tensor.restrict_rankOne line 144
  19. theorem OAI.MatrixMultiplication.Foundation.Tensor.restrict_sum line 162
  20. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.restrict line 184
  21. def OAI.MatrixMultiplication.Foundation.Tensor.pullback line 202
  22. theorem OAI.MatrixMultiplication.Foundation.Tensor.pullback_eq_restrict line 206
  23. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.pullback line 217
  24. def OAI.MatrixMultiplication.Foundation.Tensor.BorderRankAtMost line 230
  25. def OAI.MatrixMultiplication.Foundation.Tensor.restrictionOrbit line 234
  26. def OAI.MatrixMultiplication.Foundation.Tensor.DegeneratesTo line 239
  27. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.borderRankAtMost line 244
  28. theorem OAI.MatrixMultiplication.Foundation.Tensor.continuous_restrict line 248
  29. theorem OAI.MatrixMultiplication.Foundation.Tensor.BorderRankAtMost.restrict line 254
  30. theorem OAI.MatrixMultiplication.Foundation.Tensor.continuous_product_left line 268
  31. theorem OAI.MatrixMultiplication.Foundation.Tensor.continuous_product_right line 273
  32. theorem OAI.MatrixMultiplication.Foundation.Tensor.BorderRankAtMost.product line 278
  33. theorem OAI.MatrixMultiplication.Foundation.Tensor.BorderRankAtMost.of_degeneration line 299