OAI/LinearAlgebra/MatrixMultiplication/Duality/UniformInstances.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Dual matrix multiplication exponents and finite rectangular constructions.

  1. theorem OAI.MatrixMultiplication.DualUniform.coord_nonempty line 15
  2. theorem OAI.MatrixMultiplication.DualUniform.base_activeFraction line 23
  3. theorem OAI.MatrixMultiplication.DualUniform.rho2 line 30
  4. theorem OAI.MatrixMultiplication.DualUniform.rho4 line 36
  5. theorem OAI.MatrixMultiplication.DualUniform.rho8 line 42
  6. theorem OAI.MatrixMultiplication.DualUniform.rho24 line 48
  7. theorem OAI.MatrixMultiplication.DualUniform.rho48 line 54
  8. theorem OAI.MatrixMultiplication.DualUniform.rho96 line 60
  9. theorem OAI.MatrixMultiplication.DualUniform.rho288 line 66
  10. theorem OAI.MatrixMultiplication.DualUniform.laws2_uniform line 72
  11. theorem OAI.MatrixMultiplication.DualUniform.laws4_uniform line 76
  12. theorem OAI.MatrixMultiplication.DualUniform.laws8_uniform line 83
  13. theorem OAI.MatrixMultiplication.DualUniform.laws24_uniform line 91
  14. theorem OAI.MatrixMultiplication.DualUniform.laws48_uniform line 97
  15. theorem OAI.MatrixMultiplication.DualUniform.laws96_uniform line 104
  16. theorem OAI.MatrixMultiplication.DualUniform.laws288_uniform line 110