OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/InitialExact.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldInitialExact.assignedDeletion line 18
  2. theorem OAI.MatrixMultiplication.AllFieldInitialExact.assignedDeletion_eq_self_of_support line 24
  3. def OAI.MatrixMultiplication.AllFieldInitialExact.Isolated line 41
  4. theorem OAI.MatrixMultiplication.AllFieldInitialExact.assignments_on_ideal line 50
  5. theorem OAI.MatrixMultiplication.AllFieldInitialExact.branch_eq_masked_ideal line 85
  6. theorem OAI.MatrixMultiplication.AllFieldInitialExact.branch_eq_ideal line 100
  7. def OAI.MatrixMultiplication.AllFieldInitialExact.selectedExecution line 124
  8. theorem OAI.MatrixMultiplication.AllFieldInitialExact.selectedExecution_copies line 158