OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/InitialChoice.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. structure OAI.MatrixMultiplication.AllFieldInitialChoice.Choice line 17
  2. theorem OAI.MatrixMultiplication.AllFieldInitialChoice.initial_count_eq line 25
  3. theorem OAI.MatrixMultiplication.AllFieldInitialChoice.eventually_nonempty line 42
  4. abbrev OAI.MatrixMultiplication.AllFieldInitialChoice.Tags line 56
  5. theorem OAI.MatrixMultiplication.AllFieldInitialChoice.card_tags line 61
  6. def OAI.MatrixMultiplication.AllFieldInitialChoice.execution line 68
  7. theorem OAI.MatrixMultiplication.AllFieldInitialChoice.execution_copies line 77