OAI/LinearAlgebra/MatrixFields/Tensors/CWZeroGeometry.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.tensor_swapXY_inline_MatrixMultiplication_CWOrientedZero line 19
2. theorem OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.tensor_swapYZ_inline_MatrixMultiplication_CWOrientedZero line 25
3. theorem OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.tensor_swapXZ_inline_MatrixMultiplication_CWOrientedZero line 30
4. theorem OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.shape_swapXY line 34
5. theorem OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.shape_swapYZ line 47
6. theorem OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.shape_swapXZ line 60
7. def OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.placedShape line 65
8. def OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.sideWord line 68
9. def OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.matched line 72
10. theorem OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.local_coefficient line 75
11. def OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.Row line 104
12. def OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.Middle line 105
13. def OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.Column line 106
14. instance OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.(instance at line 107) line 107
15. instance OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.(instance at line 109) line 109
16. instance OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.(instance at line 111) line 111
17. theorem OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.volume line 114
18. theorem OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.matching_nonempty line 125
19. def OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.ofMatching line 166
20. theorem OAI.MatrixAllFields.MatrixMultiplication.CWOrientedZero.power_coefficient line 173
21. def OAI.MatrixAllFields.MatrixMultiplication.CWZeroGeometry.zeroAxis line 201
22. def OAI.MatrixAllFields.MatrixMultiplication.CWZeroGeometry.maxAxis line 204
23. theorem OAI.MatrixAllFields.MatrixMultiplication.CWZeroGeometry.zeroAxis_spec line 207
24. theorem OAI.MatrixAllFields.MatrixMultiplication.CWZeroGeometry.maxAxis_spec line 215
25. theorem OAI.MatrixAllFields.MatrixMultiplication.CWZeroGeometry.shapeMax_le_total line 233
26. theorem OAI.MatrixAllFields.MatrixMultiplication.CWZeroGeometry.shapeMax_pos line 237
27. theorem OAI.MatrixAllFields.MatrixMultiplication.CWZeroGeometry.zero_ne_selected line 244
28. theorem OAI.MatrixAllFields.MatrixMultiplication.CWZeroGeometry.max_add_complement line 252
29. theorem OAI.MatrixAllFields.MatrixMultiplication.CWZeroGeometry.eq_placedShape line 256
30. theorem OAI.MatrixAllFields.MatrixMultiplication.CWZeroGeometry.physicalShape_eq_placedShape line 265
31. theorem OAI.MatrixAllFields.MatrixMultiplication.CWZeroGeometry.selected_add_remaining line 277