OAI/LinearAlgebra/MatrixFields/Histories/HistoryGroupCore.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.StateWords line 22
  2. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.DueWords line 23
  3. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.CarriedWords line 24
  4. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.ActiveWords line 25
  5. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.ProducedWords line 27
  6. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.dueWordsFintype line 29
  7. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.carriedWordsFintype line 32
  8. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.activeWordsFintype line 35
  9. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.producedWordsFintype line 39
  10. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.carriedTensor line 42
  11. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.activeTensor line 48
  12. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.producedTensor line 54
  13. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.toState line 60
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.toState_due line 64
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.toState_carried line 69
  16. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.dueTensorAt line 74
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.split_coefficient line 80
  18. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.splitMap line 91
  19. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.toDue line 103
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.active_coefficient line 108
  21. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.activeMap line 119
  22. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.activeCarriedMap line 130
  23. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.fromNext line 138
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.next_coefficient line 143
  25. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRegrouping.nextMap line 155
  26. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTickCarry.distributeProduct line 192
  27. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTickCarry.liftExecution line 213
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTickCarry.liftExecution_copies line 235
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryTickCarry.liftExecution_card_copies line 242
  30. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.activeEquivOrders line 270
  31. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.activeWordsEquivOrders line 274
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.prod_active_eq_prod_orders line 285
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.familyProduct_active_eq_orders line 293
  34. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.GroupAssignment.side line 309
  35. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.GroupAssignment.restorePhysical line 312
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.GroupAssignment.side_restorePhysical line 318
  37. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.GroupAssignment.collect line 325
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.GroupAssignment.collect_eq_some line 329
  39. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.GroupAssignment.collect_failure_iff line 347
  40. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.GroupAssignment.product line 354
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.GroupAssignment.product_coherent line 362
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.GroupAssignment.product_branch line 381
  43. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.groupedSideAssignment line 411
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.groupedSideAssignment_eq_some line 416
  45. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.groupedAssignment line 423
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.groupedAssignment_coherent line 433
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.groupedAssignment_branch line 451
  48. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.joinGroupTargets line 476
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.joinGroupTargets_apply line 482
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.joinGroupTargets_on_group line 488
  51. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.joinGroupTargets_injective line 498
  52. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.groupCounts line 526
  53. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.GroupRaw line 530
  54. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.projectRaw line 535
  55. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.marginal line 539
  56. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.incoming line 547
  57. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.received line 553
  58. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.rawPass line 559
  59. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.completeKeep line 568
  60. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.marginal_project line 573
  61. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.received_project line 581
  62. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.rawPass_project line 588
  63. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.completeKeep_project line 595
  64. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.completeKeep_iff_all_groups line 604
  65. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.groupRawSource line 618
  66. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.groupPreparedSource line 627
  67. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.rawSource_factor line 635
  68. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupMasks.preparedSource_factor line 644
  69. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.deleteWithPred line 703
  70. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.Raw line 716
  71. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.toActive line 718
  72. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.parent_coefficient line 721
  73. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.receivedSource line 749
  74. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.received_coefficient line 754
  75. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.receivedMap line 785
  76. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.marginal line 796
  77. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.preparedSource line 800
  78. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.preparedSource_eq_delete line 807
  79. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.preparedMap line 819
  80. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.GroupWords line 827
  81. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.groupsEquiv line 830
  82. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.project_groups_symm line 836
  83. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.grouped_coefficient line 842
  84. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.groupsMap line 853
  85. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupedRecovery.GroupTarget line 890
  86. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupedRecovery.projectTarget line 893
  87. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupedRecovery.groupCoordinates line 897
  88. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupedRecovery.groupCoarse line 903
  89. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupedRecovery.groupIdealSide line 908