OAI/LinearAlgebra/MatrixFields/Extraction/InitialHash.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialHash.xKeep line 20
2. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialHash.yKeep line 24
3. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialHash.zKeep line 28
4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialHash.ambient_support line 32
5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialHash.target_mem_ambient line 38
6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialHash.side_survival_iff line 44
7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialHash.isolated_of_good line 52
8. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialHash.SelectedTargets line 71
9. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialHash.toTarget line 73
10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialHash.toTarget_injective line 76
11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialHash.selectedTargets_card line 79
12. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialHash.selectedExecution line 84
13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialHash.selectedExecution_copies line 99
14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialHash.exists_selectedExecution line 109