OAI/LinearAlgebra/MatrixMultiplication/Tensor/ComplexTensorRestrictionComposition.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. def OAI.MatrixMultiplication.Foundation.Tensor.composeRestrictionMatrix line 16
  2. theorem OAI.MatrixMultiplication.Foundation.Tensor.sum_three_mul line 20
  3. theorem OAI.MatrixMultiplication.Foundation.Tensor.sum_six_comm line 29
  4. theorem OAI.MatrixMultiplication.Foundation.Tensor.sum_interleaved_triples line 42
  5. theorem OAI.MatrixMultiplication.Foundation.Tensor.restrict_restrict line 63
  6. theorem OAI.MatrixMultiplication.Foundation.Tensor.restrict_product line 97
  7. theorem OAI.MatrixMultiplication.Foundation.Tensor.restrict_identity line 133
  8. theorem OAI.MatrixMultiplication.Foundation.Tensor.degeneratesTo_restrict line 152
  9. theorem OAI.MatrixMultiplication.Foundation.Tensor.DegeneratesTo.refl line 157
  10. theorem OAI.MatrixMultiplication.Foundation.Tensor.mem_restrictionOrbit_restrict line 166
  11. theorem OAI.MatrixMultiplication.Foundation.Tensor.DegeneratesTo.restrict line 174
  12. theorem OAI.MatrixMultiplication.Foundation.Tensor.DegeneratesTo.trans line 187
  13. theorem OAI.MatrixMultiplication.Foundation.Tensor.DegeneratesTo.of_restrict line 196