OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/ProducedMaskCore.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. def OAI.MatrixMultiplication.AllFieldHistoryProducedMasks.nativeChildWidth line 21
  2. def OAI.MatrixMultiplication.AllFieldHistoryProducedMasks.halfPositionEquiv line 24
  3. def OAI.MatrixMultiplication.AllFieldHistoryProducedMasks.childHalfWord line 33
  4. theorem OAI.MatrixMultiplication.AllFieldHistoryProducedMasks.subsingleton_typeWindow line 41
  5. theorem OAI.MatrixMultiplication.AllFieldHistoryProducedMasks.childHalfWord_window line 56
  6. theorem OAI.MatrixMultiplication.AllFieldHistoryProducedMasks.afterB_mask_of_part_masks line 105
  7. def OAI.MatrixMultiplication.AllFieldHistoryProducedMasks.producedChildWord line 134
  8. theorem OAI.MatrixMultiplication.AllFieldHistoryProducedMasks.producedChildWord_mask line 149
  9. theorem OAI.MatrixMultiplication.AllFieldHistoryProducedMasks.splitWord_eq_of_position line 172
  10. theorem OAI.MatrixMultiplication.AllFieldHistoryProducedMasks.producedHalfWord_eq_childHalfWord line 183
  11. theorem OAI.MatrixMultiplication.AllFieldHistoryProducedMasks.producedHalfWord_window line 224
  12. theorem OAI.MatrixMultiplication.AllFieldHistoryProducedMasks.regroupBranch_window line 238
  13. theorem OAI.MatrixMultiplication.AllFieldHistoryProducedMasks.canonicalWindows_of_produced_masks line 261