OAI/LinearAlgebra/MatrixMultiplication/Duality/WitnessProgram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Dual matrix multiplication exponents and finite rectangular constructions.

  1. abbrev OAI.MatrixMultiplication.DualWitness.Word line 16
  2. def OAI.MatrixMultiplication.DualWitness.source line 17
  3. abbrev OAI.MatrixMultiplication.DualWitness.Support line 18
  4. def OAI.MatrixMultiplication.DualWitness.readable line 20
  5. def OAI.MatrixMultiplication.DualWitness.program line 23
  6. theorem OAI.MatrixMultiplication.DualWitness.program_complete line 26
  7. theorem OAI.MatrixMultiplication.DualWitness.record_injective line 30
  8. def OAI.MatrixMultiplication.DualWitness.x line 35
  9. theorem OAI.MatrixMultiplication.DualWitness.coord_card line 37
  10. theorem OAI.MatrixMultiplication.DualWitness.word_card line 47