OAI/Analysis/MatrixSigning/Arithmetic/RationalBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W30.divInt_num_natAbs_le line 11
2. theorem OAI.KS.W30.divInt_den_le line 17
3. theorem OAI.KS.W30.divInt_num_size_le line 21
4. theorem OAI.KS.W30.divInt_den_size_le line 25
5. theorem OAI.KS.W30.matrix_den_dvd_prod line 29
6. theorem OAI.KS.W30.matrix_den_le_prod line 36
7. theorem OAI.KS.W30.matrix_den_le_two_pow line 43
8. theorem OAI.KS.W30.cleared_matrix_entry line 52
9. theorem OAI.KS.W30.cleared_num_natAbs_le line 59
10. theorem OAI.KS.W30.cleared_num_le_two_pow line 77