OAI/LinearAlgebra/MatrixFields/Parameters/ParametersHalfComplement.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.normalized_singleton_law line 14
2. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.pairWeight_zero line 28
3. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.pairWeight_eight line 31
4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.pairKappa_zero line 34
5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.pairKappa_eight line 37
6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.halfLaw_weight_zero line 40
7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.halfLaw_weight_eight line 49
8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.complementary_half_sides_zero_parent line 58
9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.halfLaw_complementary_sides line 61
10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.zero_maximum_axis_nonzero line 75
11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.halfLaw_at_maximum line 78
12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.zeroPairLaw_shapeMax_eight line 84