OAI/LinearAlgebra/MatrixMultiplication/Tensor/ComplexTensorFlattening.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.card_le_of_identity line 17
  2. theorem OAI.MatrixMultiplication.Foundation.Tensor.directSum_matrixCoefficients_rank_lower line 38
  3. theorem OAI.MatrixMultiplication.Foundation.Tensor.directSum_square_rank_lower line 58