OAI/LinearAlgebra/MatrixMultiplication/Tensor/ComplexLocalMaps.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. def OAI.MatrixMultiplication.Foundation.LocalMaps.fiberMatrix line 16
  2. def OAI.MatrixMultiplication.Foundation.LocalMaps.fiberTransform line 20
  3. def OAI.MatrixMultiplication.Foundation.LocalMaps.originalScale line 27
  4. theorem OAI.MatrixMultiplication.Foundation.LocalMaps.fiberTransform_originalScale line 32
  5. theorem OAI.MatrixMultiplication.Foundation.LocalMaps.fiberTransform_substitution line 48
  6. theorem OAI.MatrixMultiplication.Foundation.LocalMaps.fiberTransform_eq_restrict line 59
  7. def OAI.MatrixMultiplication.Foundation.LocalMaps.originalMask line 69
  8. theorem OAI.MatrixMultiplication.Foundation.LocalMaps.fiberTransform_originalMask line 75
  9. def OAI.MatrixMultiplication.Foundation.LocalMaps.SupportedOn line 84
  10. theorem OAI.MatrixMultiplication.Foundation.LocalMaps.fiberTransform_supportedOn line 88
  11. theorem OAI.MatrixMultiplication.Foundation.LocalMaps.originalMask_eq_self line 102
  12. def OAI.MatrixMultiplication.Foundation.LocalMaps.localSelector line 111
  13. theorem OAI.MatrixMultiplication.Foundation.LocalMaps.factoredMask_eq_restrict line 116
  14. def OAI.MatrixMultiplication.Foundation.LocalMaps.Synchronized line 128
  15. def OAI.MatrixMultiplication.Foundation.LocalMaps.InBranch line 132
  16. theorem OAI.MatrixMultiplication.Foundation.LocalMaps.factoredMask_synchronized line 137
  17. theorem OAI.MatrixMultiplication.Foundation.LocalMaps.controlled_eq_sum_branches line 155
  18. theorem OAI.MatrixMultiplication.Foundation.LocalMaps.controlled_eq_sum_branches_of_supported line 181