OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/InitialHistories.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. theorem OAI.MatrixMultiplication.AllFieldHistory.shapeCounts_fiber line 14
  2. def OAI.MatrixMultiplication.AllFieldHistory.shapeCountFiberEquiv line 21
  3. abbrev OAI.MatrixMultiplication.AllFieldHistory.InitialPlacement line 28
  4. abbrev OAI.MatrixMultiplication.AllFieldHistory.InitialShapeFiber line 30
  5. def OAI.MatrixMultiplication.AllFieldHistory.initialClassPositionEquiv line 33
  6. theorem OAI.MatrixMultiplication.AllFieldHistory.initialClassPosition_shape line 40
  7. def OAI.MatrixMultiplication.AllFieldHistory.initialStateEquiv line 47