OAI/LinearAlgebra/MatrixFields/Parameters/ComplementSums.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.placements line 12
2. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.initialMultiplicity_counts_placements line 17
3. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.parents_nodup line 20
4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.split_keys_nodup line 23
5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.binary_keys_nodup line 26
6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.pair_keys_nodup line 28
7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageA_children_nodup line 30
8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageB_children_nodup line 32
9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.ordered_pairs_nodup line 34
10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.initial_placements_partition line 36
11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.list_map_involution_perm line 46
12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.list_weighted_involution_sum line 61
13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.complement_involution_of_le line 76
14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageA_complement_sum line 81
15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageB_complement_sum line 94