OAI/LinearAlgebra/MatrixMultiplication/Tensor/ComplexEqualSummandASI.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_rank_of_injective line 22
  2. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_directSum_rank_of_injective line 34
  3. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_directSum_power_rank line 48
  4. theorem OAI.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.square_directSum_power_rank line 60
  5. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_fin_one_rank line 68
  6. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_pow_batchRank line 80
  7. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.rpow_omega_le_of_rankAtMost line 101
  8. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.rpow_omega_le_of_rank_growth line 117
  9. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.equalSummand_inequality_of_quadratic_bound line 142
  10. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.equalSummand_inequality line 164
  11. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.equalSummand_inequality_of_polynomialApproximation line 183