OAI/LinearAlgebra/MatrixMultiplication/ComplexBounds/CW75ReorderedGeometricValues.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Explicit complex square and rectangular matrix multiplication bounds.

  1. abbrev OAI.MatrixMultiplication.CW75ReorderedGeometricValues.size line 22
  2. theorem OAI.MatrixMultiplication.CW75ReorderedGeometricValues.actualPool_decode line 24
  3. theorem OAI.MatrixMultiplication.CW75ReorderedGeometricValues.decode_eq_iff_eligible line 30
  4. theorem OAI.MatrixMultiplication.CW75ReorderedGeometricValues.first_read line 39
  5. theorem OAI.MatrixMultiplication.CW75ReorderedGeometricValues.second_read line 46
  6. theorem OAI.MatrixMultiplication.CW75ReorderedGeometricValues.raw_XY_normal line 53
  7. theorem OAI.MatrixMultiplication.CW75ReorderedGeometricValues.raw_XZ_normal line 81
  8. theorem OAI.MatrixMultiplication.CW75ReorderedGeometricValues.raw_YZ_normal line 116