OAI/Analysis/MatrixSigning/Matrices/DeterminantBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W30.factorial_le_two_pow_sq line 11
2. theorem OAI.KS.W30.abs_det_le line 17
3. theorem OAI.KS.W30.natAbs_det_le line 23
4. theorem OAI.KS.W30.natAbs_det_le_two_pow line 34
5. theorem OAI.KS.W30.size_natAbs_det_le line 43
6. theorem OAI.KS.W30.abs_adjugate_le line 53
7. theorem OAI.KS.W30.natAbs_adjugate_le line 67
8. theorem OAI.KS.W30.natAbs_adjugate_le_two_pow line 78