OAI/LinearAlgebra/MatrixFields/Construction/GroupAssignments.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupSourceSupport.masks_of_prepared line 26
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupSourceSupport.raw_nonzero line 37
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupSourceSupport.marginal_sideMask line 45
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupSourceSupport.marginal_source_nonzero line 57
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupSourceSupport.prepared_source_support line 73
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.physical_coarseMask line 114
  7. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.halfShape line 130
  8. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.halfLaw line 134
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.physical_half_product_nonzero line 138
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.priority_half_product_nonzero line 177
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.useful_half_window line 198
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.own_coarse_guard line 212
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.transferY line 225
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCompatibilityTransfer.transferZ line 253
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAssignments.actualCompatible_own line 322
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAssignments.physicalAssignment_coherent line 331