OAI/LinearAlgebra/MatrixMultiplication/Duality/ScriptIndependence.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Dual matrix multiplication exponents and finite rectangular constructions.

  1. theorem OAI.MatrixMultiplication.DualProgramIndependence.minusLaws_independent line 24
  2. theorem OAI.MatrixMultiplication.DualProgramIndependence.plusALaws_independent line 41
  3. theorem OAI.MatrixMultiplication.DualProgramIndependence.plusCLaws_independent line 60
  4. abbrev OAI.MatrixMultiplication.DualProgramIndependence.dualReadable line 79
  5. theorem OAI.MatrixMultiplication.DualProgramIndependence.base_independent line 82
  6. theorem OAI.MatrixMultiplication.DualProgramIndependence.laws2_independent line 87
  7. theorem OAI.MatrixMultiplication.DualProgramIndependence.laws4_independent line 91
  8. theorem OAI.MatrixMultiplication.DualProgramIndependence.laws8_independent line 95
  9. theorem OAI.MatrixMultiplication.DualProgramIndependence.laws24_independent line 99
  10. theorem OAI.MatrixMultiplication.DualProgramIndependence.laws48_independent line 103
  11. theorem OAI.MatrixMultiplication.DualProgramIndependence.laws96_independent line 107
  12. theorem OAI.MatrixMultiplication.DualProgramIndependence.laws288_independent line 111