OAI/LinearAlgebra/MatrixFields/Tensors/ComplexDotPairing.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor line 14
  2. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.rankOne line 22
  3. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost line 25
  4. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.restrict line 29
  5. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.contract line 35
  6. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.product line 39
  7. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.directSum line 43
  8. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.power line 47
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.directSum_matching line 51
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.directSum_zero_of_left_ne line 56
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.rankAtMost_zero line 61
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.rankOne_rankAtMost line 66
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.map line 72
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.scale line 80
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.rankAtMost_sum_rankOne line 88
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.product line 100
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.power line 124
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.restrict_rankOne line 142
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.restrict_sum line 160
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.restrict line 182
  21. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.pullback line 200
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.pullback_eq_restrict line 204
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.pullback line 215
  24. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.BorderRankAtMost line 228
  25. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.restrictionOrbit line 232
  26. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.DegeneratesTo line 237
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.borderRankAtMost line 242
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.continuous_restrict line 246
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.BorderRankAtMost.restrict line 252
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.continuous_product_left line 266
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.continuous_product_right line 271
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.BorderRankAtMost.product line 276
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.BorderRankAtMost.of_degeneration line 297
  34. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.diagonal line 329
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.diagonal_rankAtMost line 332
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.repeat_batch line 343
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.batch_substitute line 381
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.batch_product line 402
  39. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.composeRestrictionMatrix line 430
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.sum_three_mul line 434
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.sum_six_comm line 443
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.sum_interleaved_triples line 456
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.restrict_restrict line 477
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.restrict_product line 511
  45. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.restrict_identity line 547
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.degeneratesTo_restrict line 564
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.DegeneratesTo.refl line 569
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.mem_restrictionOrbit_restrict line 578
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.DegeneratesTo.restrict line 586
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.DegeneratesTo.trans line 599
  51. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.DegeneratesTo.of_restrict line 608
  52. theorem OAI.MatrixAllFields.MatrixMultiplication.Replication.restrict_directSum line 634
  53. theorem OAI.MatrixAllFields.MatrixMultiplication.Replication.swap_replication line 661
  54. theorem OAI.MatrixAllFields.MatrixMultiplication.Replication.repair_branches line 673
  55. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.groupTensor line 707
  56. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.groupTensor_fourier line 709
  57. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.groupTensor_rankAtMost line 729
  58. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.dotPairing line 757
  59. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.dotPairing_matching line 760
  60. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.contract_dotPairing line 764