OAI/LinearAlgebra/MatrixFields/Arithmetic/ComplexArithmeticExponent.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Expression.sumFin line 20
2. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Expression.sumFin_eval line 24
3. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Expression.sumFin_cost line 30
4. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.naiveEntry line 40
5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.naiveEntry_eval line 44
6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.naiveEntry_cost line 49
7. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.naiveAlgorithm line 53
8. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.naiveAlgorithm_correct line 59
9. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.naiveAlgorithm_cost line 67
10. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.naiveAlgorithm_cost_le line 75
11. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_three line 78
12. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_nonempty line 96
13. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.AdmissibleExponent.mono line 107
14. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.omega_le_of_admissibleExponent line 119
15. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.omega_nonneg line 123
16. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.omega_le_three line 126
17. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.omega_admissibleExponent line 129
18. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_iff_omega_le line 143