OAI/LinearAlgebra/MatrixMultiplication/Duality/ProgramIndependence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Dual matrix multiplication exponents and finite rectangular constructions.

  1. theorem OAI.MatrixMultiplication.DualProgramIndependence.independentProduct_triple_mass line 27
  2. theorem OAI.MatrixMultiplication.DualProgramIndependence.independentProduct_factorization line 43
  3. theorem OAI.MatrixMultiplication.DualProgramIndependence.factorization_constant_label line 65
  4. theorem OAI.MatrixMultiplication.DualProgramIndependence.colorSlice_context_mass line 84
  5. theorem OAI.MatrixMultiplication.DualProgramIndependence.colorMix_context_mass line 96
  6. theorem OAI.MatrixMultiplication.DualProgramIndependence.colorMix_refined_context_mass line 105
  7. theorem OAI.MatrixMultiplication.DualProgramIndependence.colorMix_factorization line 120
  8. theorem OAI.MatrixMultiplication.DualProgramIndependence.colorMix_recorded_factorization line 153
  9. def OAI.MatrixMultiplication.DualProgramIndependence.ProgramLawsIndependent line 181