OAI/LinearAlgebra/MatrixMultiplication/Duality/RootIndependence.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Dual matrix multiplication exponents and finite rectangular constructions.

  1. theorem OAI.MatrixMultiplication.DualProgramIndependence.rootColor_inj_before_three line 19
  2. theorem OAI.MatrixMultiplication.DualProgramIndependence.completion_index_decomposition line 23
  3. theorem OAI.MatrixMultiplication.DualProgramIndependence.conditionalCompletionLaw_pattern_factorization line 43
  4. theorem OAI.MatrixMultiplication.DualProgramIndependence.conditionalCompletionLaw_root_factorization line 91
  5. theorem OAI.MatrixMultiplication.DualProgramIndependence.conditionalCompletionLaw_program_factorization line 150