OAI/LinearAlgebra/MatrixFields/Construction/ActiveSums.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.aRelot line 18
  2. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.bRelot line 21
  3. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.partRelot line 24
  4. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.workRelot line 27
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.workRelot_lot line 32
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.workRelot_stage line 35
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.workRelot_self line 38
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.workRelot_relot line 41
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.workAmount_relot line 45
  10. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.workLotEquiv line 50
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.workLotEquiv_symm_apply line 62
  12. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.workStagesEquiv line 65
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.work_sum line 78
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.sum_lot_tick line 89
  15. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.shapeValue line 104
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.shapeValue_relot line 110
  17. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageASourceSum line 115
  18. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageBSourceSum line 118
  19. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCSourceSum line 121
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageA_one_lot_sum line 125
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageB_one_lot_sum line 131
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageC_one_lot_sum line 136
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.subtype_sum_indicator_inline_MatrixMultiplication_AllFieldActiveSums line 145
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.active_shape_sum line 151
  25. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.shapeCapacity line 179
  26. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageASourceCapacity line 183
  27. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageBSourceCapacity line 186
  28. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCSourceCapacity line 189
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.activeAggregateCapacity_shapeCapacity line 193