OAI/LinearAlgebra/MatrixFields/Construction/ComplexLocalMaps.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.fiberMatrix line 19
2. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.fiberTransform line 23
3. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.originalScale line 30
4. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.fiberTransform_originalScale line 35
5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.fiberTransform_substitution line 51
6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.fiberTransform_eq_restrict line 62
7. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.originalMask line 72
8. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.fiberTransform_originalMask line 78
9. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.SupportedOn line 87
10. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.fiberTransform_supportedOn line 91
11. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.originalMask_eq_self line 105
12. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.localSelector line 114
13. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.factoredMask_eq_restrict line 119
14. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.Synchronized line 131
15. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.InBranch line 135
16. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.factoredMask_synchronized line 140
17. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.controlled_eq_sum_branches line 158
18. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.LocalMaps.controlled_eq_sum_branches_of_supported line 184