OAI/LinearAlgebra/MatrixMultiplication/ComplexBounds/CW75ReorderedWords.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Explicit complex square and rectangular matrix multiplication bounds.

  1. abbrev OAI.MatrixMultiplication.CW75ReorderedWords.BlockPosition line 18
  2. abbrev OAI.MatrixMultiplication.CW75ReorderedWords.LongWord line 22
  3. def OAI.MatrixMultiplication.CW75ReorderedWords.longX line 24
  4. def OAI.MatrixMultiplication.CW75ReorderedWords.longY line 25
  5. def OAI.MatrixMultiplication.CW75ReorderedWords.longZ line 26
  6. def OAI.MatrixMultiplication.CW75ReorderedWords.longCoordinate line 28
  7. def OAI.MatrixMultiplication.CW75ReorderedWords.coordinateOf line 31
  8. theorem OAI.MatrixMultiplication.CW75ReorderedWords.coordinateOf_original line 38
  9. theorem OAI.MatrixMultiplication.CW75ReorderedWords.longCoordinates_injective line 44
  10. def OAI.MatrixMultiplication.CW75ReorderedWords.Represents line 55
  11. def OAI.MatrixMultiplication.CW75ReorderedWords.eligible line 60
  12. def OAI.MatrixMultiplication.CW75ReorderedWords.firstRead line 64
  13. def OAI.MatrixMultiplication.CW75ReorderedWords.secondRead line 68
  14. theorem OAI.MatrixMultiplication.CW75ReorderedWords.firstRead_on_original_word line 72
  15. theorem OAI.MatrixMultiplication.CW75ReorderedWords.secondRead_on_original_word line 84
  16. theorem OAI.MatrixMultiplication.CW75ReorderedWords.readers_recover_original_fine line 96
  17. theorem OAI.MatrixMultiplication.CW75ReorderedWords.readable_of_eligible line 111
  18. theorem OAI.MatrixMultiplication.CW75ReorderedWords.represented_word_unique line 120
  19. theorem OAI.MatrixMultiplication.CW75ReorderedWords.eligible_coefficient_one line 130
  20. theorem OAI.MatrixMultiplication.CW75ReorderedWords.eligible_original_grade line 138
  21. theorem OAI.MatrixMultiplication.CW75ReorderedWords.eligible_appendCode_iff line 146
  22. theorem OAI.MatrixMultiplication.CW75ReorderedWords.represented_fine_eq line 174
  23. theorem OAI.MatrixMultiplication.CW75ReorderedWords.eligible_appendCode_iff_of_represents line 182
  24. theorem OAI.MatrixMultiplication.CW75ReorderedWords.root_eligible_iff line 196
  25. def OAI.MatrixMultiplication.CW75ReorderedWords.terminalWord line 218
  26. theorem OAI.MatrixMultiplication.CW75ReorderedWords.terminalWord_record line 229
  27. theorem OAI.MatrixMultiplication.CW75ReorderedWords.terminalWord_of_represents line 233
  28. theorem OAI.MatrixMultiplication.CW75ReorderedWords.terminal_eligible_iff line 240
  29. theorem OAI.MatrixMultiplication.CW75ReorderedWords.terminal_original_grade line 254
  30. theorem OAI.MatrixMultiplication.CW75ReorderedWords.stage0_XY_readable line 262
  31. theorem OAI.MatrixMultiplication.CW75ReorderedWords.stage1_XZ_readable line 269
  32. theorem OAI.MatrixMultiplication.CW75ReorderedWords.stage2_XY_readable line 276
  33. theorem OAI.MatrixMultiplication.CW75ReorderedWords.stage3_YZ_readable line 283
  34. theorem OAI.MatrixMultiplication.CW75ReorderedWords.stage4_YZ_readable line 290