OAI/Analysis/MatrixSigning/Machines/InverseBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W30.integer_matrix_inverse_entry line 13
2. theorem OAI.KS.W30.integer_inverse_parts_size_le line 25
3. theorem OAI.KS.W30.rational_matrix_inverse_entry line 41
4. theorem OAI.KS.W30.cleared_det_ne_zero line 56
5. theorem OAI.KS.W30.rational_inverse_parts_size_le line 69
6. theorem OAI.KS.W30.rational_inverse_parts_size_le_fintype line 99