OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/InitialOrbit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. theorem OAI.MatrixMultiplication.AllFieldInitialOrbit.source_total line 12
  2. theorem OAI.MatrixMultiplication.AllFieldInitialOrbit.decodeShape_injective line 19
  3. theorem OAI.MatrixMultiplication.AllFieldInitialOrbit.decodeShape_mem_shapes line 27
  4. theorem OAI.MatrixMultiplication.AllFieldInitialOrbit.initialShapeCode_eq_iff line 39
  5. theorem OAI.MatrixMultiplication.AllFieldInitialOrbit.weighted_shape_fiber_count line 49
  6. theorem OAI.MatrixMultiplication.AllFieldInitialOrbit.weighted_fiber_count line 55