OAI/LinearAlgebra/MatrixMultiplication/FieldGroups/CompatibilityTransfer.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Group assignments, orbit counts and extraction capacities.

  1. theorem OAI.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.physical_coarseMask line 23
  2. def OAI.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.halfShape line 39
  3. def OAI.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.halfLaw line 43
  4. theorem OAI.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.physical_half_product_nonzero line 47
  5. theorem OAI.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.priority_half_product_nonzero line 86
  6. theorem OAI.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.useful_half_window line 107
  7. theorem OAI.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.own_coarse_guard line 121
  8. theorem OAI.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.transferY line 134
  9. theorem OAI.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.transferZ line 162