OAI/LinearAlgebra/MatrixFields/Tensors/TerminalRelabel.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients line 18
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixMultiplication_eq_matrixCoefficients line 22
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.contract_matrixCoefficients line 25
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_product line 32
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_cyclic line 43
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_rank_of_product line 51
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_product_rank line 71
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_batch_rank line 78
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_power line 86
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_cyclic_rank line 94
  11. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.cyclic line 118
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.cyclic line 121
  13. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.directSumProductEquiv line 131
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.directSum_product line 138
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.directSum_product line 169
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.directSum_pullback line 178
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.directSum_pullback line 184
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.cyclic_directSum line 191
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.directSum_cyclic line 209
  20. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.directSumPowerEquiv line 215
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.directSum_power line 222
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.directSum_const_power line 235
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.directSum_const_of_power line 242
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.directSum_const_power line 251
  25. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.rectangularSquareX line 260
  26. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.rectangularSquareY line 267
  27. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.rectangularSquareZ line 274
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_directSum_rank_of_power line 283
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_cyclic_product_square line 303
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.cyclic_matrixCoefficients line 317
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_symmetrized_rank line 322
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_directSum_symmetrized_rank line 332
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.symmetrized_tag_card line 345
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.symmetrized_index_card line 350
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.card_le_of_identity line 374
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.directSum_matrixCoefficients_rank_lower line 395
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.directSum_square_rank_lower line 415
  38. def OAI.MatrixAllFields.MatrixMultiplication.TerminalRelabel.taggedPair line 438
  39. theorem OAI.MatrixAllFields.MatrixMultiplication.TerminalRelabel.directSum_matrix_pullback line 442
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.TerminalRelabel.directSum_matrix_restrict_equiv line 453
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.TerminalRelabel.exists_directSum_matrix_restrict_equiv line 467
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.TerminalRelabel.directSum_matrix_restrict_of_card_eq line 480
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.TerminalRelabel.directSum_matrix_restrict_fin line 496