OAI/LinearAlgebra/MatrixFields/Extraction/JointExtraction.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MatrixAllFields.MatrixMultiplication.JointExtraction.Assignment line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.JointExtraction.uniqueAssignment line 21
3. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtraction.uniqueAssignment_spec line 28
4. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtraction.uniqueAssignment_unique line 39
5. def OAI.MatrixAllFields.MatrixMultiplication.JointExtraction.retainAssignment line 45
6. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtraction.retainAssignment_some line 50
7. def OAI.MatrixAllFields.MatrixMultiplication.JointExtraction.Coherent line 58
8. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtraction.coherent_of_sequential line 62
9. def OAI.MatrixAllFields.MatrixMultiplication.JointExtraction.branch line 77
10. def OAI.MatrixAllFields.MatrixMultiplication.JointExtraction.assignmentMatrix line 83
11. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtraction.restrict_assignments_apply line 88
12. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtraction.restrict_assignments_eq_directSum line 99
13. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtraction.rankAtMost_directSum_branches line 125
14. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtraction.coherent_of_support_subset line 133