OAI/LinearAlgebra/MatrixMultiplication/Rectangular/Recursion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Rectangular matrix multiplication algorithms and their asymptotic exponents.

  1. theorem OAI.MatrixMultiplication.Tensor.rectangular_rank_of_injective line 17
  2. theorem OAI.MatrixMultiplication.Tensor.rectangular_directSum_rank_of_injective line 33
  3. theorem OAI.MatrixMultiplication.Tensor.rectangular_directSum_power_rank line 53
  4. theorem OAI.MatrixMultiplication.Tensor.rectangular_pow_batchRank line 67
  5. theorem OAI.MatrixMultiplication.Tensor.rectangular_polynomial_power_rank line 89
  6. theorem OAI.MatrixMultiplication.Tensor.rectangular_directSum_cyclic_rank line 98
  7. theorem OAI.MatrixMultiplication.Tensor.rectangular_directSum_rank_lower line 124