OAI/LinearAlgebra/MatrixFields/Extraction/AuxiliarySeparation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.MatrixAllFields.MatrixMultiplication.Foundation.auxiliarySeparation_modulus_neZero line 13
2. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.auxiliary_separation_mem_restrictionOrbit line 23
3. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.auxiliary_separation_rankAtMost line 35
4. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.auxiliary_separation_borderRankAtMost line 47
5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.auxiliary_separation_directSum_rankAtMost line 60
6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.auxiliary_separation_directSum_borderRankAtMost line 71
7. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.auxiliary_separation_logarithmic_cost line 85
8. theorem OAI.MatrixAllFields.MatrixMultiplication.AuxiliarySeparation.directSum_rankAtMost line 104
9. theorem OAI.MatrixAllFields.MatrixMultiplication.AuxiliarySeparation.directSum_borderRankAtMost line 114
10. theorem OAI.MatrixAllFields.MatrixMultiplication.AuxiliarySeparation.logarithmic_cost line 124
11. theorem OAI.MatrixAllFields.MatrixMultiplication.AuxiliarySeparation.cost_minus_population_tendsto_zero line 129