OAI/LinearAlgebra/MatrixMultiplication/Duality/CompletionLaws.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Dual matrix multiplication exponents and finite rectangular constructions.

  1. abbrev OAI.MatrixMultiplication.DualCompletionLaws.Laws line 22
  2. def OAI.MatrixMultiplication.DualCompletionLaws.gibbsWeight line 24
  3. theorem OAI.MatrixMultiplication.DualCompletionLaws.gibbsWeight_nonneg line 26
  4. theorem OAI.MatrixMultiplication.DualCompletionLaws.gibbsWeight_lt_one line 29
  5. def OAI.MatrixMultiplication.DualCompletionLaws.minusLaws line 33
  6. def OAI.MatrixMultiplication.DualCompletionLaws.plusALaws line 39
  7. def OAI.MatrixMultiplication.DualCompletionLaws.plusCLaws line 47
  8. def OAI.MatrixMultiplication.DualCompletionLaws.baseLeaf line 55
  9. def OAI.MatrixMultiplication.DualCompletionLaws.baseLaws line 63
  10. def OAI.MatrixMultiplication.DualCompletionLaws.script2 line 65
  11. def OAI.MatrixMultiplication.DualCompletionLaws.script4 line 66
  12. def OAI.MatrixMultiplication.DualCompletionLaws.script8 line 67
  13. def OAI.MatrixMultiplication.DualCompletionLaws.script24 line 68
  14. def OAI.MatrixMultiplication.DualCompletionLaws.script48 line 69
  15. def OAI.MatrixMultiplication.DualCompletionLaws.script96 line 70
  16. def OAI.MatrixMultiplication.DualCompletionLaws.laws2 line 72
  17. def OAI.MatrixMultiplication.DualCompletionLaws.laws4 line 75
  18. def OAI.MatrixMultiplication.DualCompletionLaws.laws8 line 81
  19. def OAI.MatrixMultiplication.DualCompletionLaws.laws24 line 89
  20. def OAI.MatrixMultiplication.DualCompletionLaws.laws48 line 95
  21. def OAI.MatrixMultiplication.DualCompletionLaws.laws96 line 101
  22. def OAI.MatrixMultiplication.DualCompletionLaws.laws288 line 107