OAI/LinearAlgebra/MatrixFields/Histories/HistoryIteration.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.CanonicalWords line 23
  2. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.ProducedWords line 26
  3. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.CanonicalClassPosition line 29
  4. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.CanonicalHalfPosition line 32
  5. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.canonicalClassEquiv line 35
  6. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.splitArrangeEquiv line 42
  7. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.canonicalSplitEquiv line 51
  8. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.canonicalProducedEquiv line 60
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.splitProduced_length line 66
  10. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.splitWord line 73
  11. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.producedHalfWord line 79
  12. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.regroupAt line 84
  13. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.regroupWords line 89
  14. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.branchClassEquiv line 94
  15. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.branchClassIndex line 106
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.regroupWords_branch line 111
  17. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.canonicalHalfShape line 128
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.canonicalProduced_length line 133
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.canonicalProduced_shape line 139
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.shapeTensor_finCast line 176
  21. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.canonicalChildren line 183
  22. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.producedBase line 191
  23. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.canonicalHalfWord line 199
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.regroupWords_half line 204
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.canonicalChildren_flat line 211
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.producedBase_flat line 226
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.regroup_coefficient_at line 235
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.regroup_coefficient line 249
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.regroup_pullback line 259
  30. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.regroupMatrix line 266
  31. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.producedBaseMap line 271
  32. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProducedMasks.nativeChildWidth line 307
  33. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProducedMasks.halfPositionEquiv line 310
  34. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProducedMasks.childHalfWord line 319
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProducedMasks.subsingleton_typeWindow line 327
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProducedMasks.childHalfWord_window line 342
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProducedMasks.afterB_mask_of_part_masks line 391
  38. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProducedMasks.producedChildWord line 420
  39. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProducedMasks.producedChildWord_mask line 435
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProducedMasks.splitWord_eq_of_position line 458
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProducedMasks.producedHalfWord_eq_childHalfWord line 469
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProducedMasks.producedHalfWord_window line 510
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProducedMasks.regroupBranch_window line 524
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProducedMasks.canonicalWindows_of_produced_masks line 547
  45. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProducedMasks.childWindows_of_produced_masks line 601
  46. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProduced.passes line 632
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProduced.producedTensor_eq_delete line 636
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProduced.canonical_eq_delete line 645
  49. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProduced.pulled line 669
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProduced.delete_pulled line 677
  51. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProduced.pullbackMap line 696
  52. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryProduced.map line 705
  53. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.Choices line 738
  54. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.AmbientTag line 741
  55. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.Tags line 745
  56. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.coarseTripleFintype line 751
  57. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.ambientTagFintype line 754
  58. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.ambientTagsFintype line 758
  59. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.tagsFintype line 761
  60. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.select line 764
  61. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.select_injective line 769
  62. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.targets line 777
  63. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.assignments line 782
  64. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.assignment line 791
  65. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.coherent line 795
  66. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.repair line 805
  67. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.canonicalMap line 842
  68. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.activeExecution line 856
  69. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.activeExecution_copies line 877
  70. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.card_tags line 887
  71. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.execution line 896
  72. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTick.execution_copies line 905
  73. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIteration.retarget line 938
  74. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIteration.retarget_copies line 949
  75. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIteration.ScheduleChoices line 956
  76. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIteration.Labels line 959
  77. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIteration.labelsFintype line 967
  78. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIteration.card_labels line 978
  79. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIteration.Tags line 996
  80. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIteration.card_tags line 1000
  81. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIteration.run line 1016
  82. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIteration.run_copies line 1033
  83. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIteration.execution line 1047
  84. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIteration.execution_copies line 1053