OAI/LinearAlgebra/MatrixMultiplication/ComplexBounds/CW75ReorderedRectangular.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Explicit complex square and rectangular matrix multiplication bounds.

  1. theorem OAI.MatrixMultiplication.CW75ReorderedRectangular.rectangularOmega_lt_target line 14