OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/MaskLaws.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. def OAI.MatrixMultiplication.AllFieldHistoryMaskLaws.parentCenter line 20
  2. theorem OAI.MatrixMultiplication.AllFieldHistoryMaskLaws.center_eq_parentCenter line 27
  3. def OAI.MatrixMultiplication.AllFieldHistoryMaskLaws.stageBActive line 58
  4. theorem OAI.MatrixMultiplication.AllFieldHistoryMaskLaws.stageB_leftLaw_branch line 62
  5. theorem OAI.MatrixMultiplication.AllFieldHistoryMaskLaws.stageB_rightLaw_branch line 72
  6. theorem OAI.MatrixMultiplication.AllFieldHistoryMaskLaws.stageB_sum_laws line 83
  7. theorem OAI.MatrixMultiplication.AllFieldHistoryMaskLaws.parentCenter_stageB line 99
  8. theorem OAI.MatrixMultiplication.AllFieldHistoryMaskLaws.center_stageB line 137