OAI/Probability/SignedSweeps/HookArms.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.IsSignedHook line 9
  2. lemma OAI.SignedSweeps.signedHook_no_southeast line 11
  3. lemma OAI.SignedSweeps.IsSignedHook.transpose line 21
  4. lemma OAI.SignedSweeps.signedHook_colLen_le line 28
  5. lemma OAI.SignedSweeps.rowLen_le_card line 34
  6. lemma OAI.SignedSweeps.colLen_le_card line 38
  7. lemma OAI.SignedSweeps.boxHook_le_twice_card line 42
  8. def OAI.SignedSweeps.rightHookProduct line 49
  9. lemma OAI.SignedSweeps.prod_right_cells line 52
  10. lemma OAI.SignedSweeps.right_hook_le line 88
  11. lemma OAI.SignedSweeps.arm_factorial_bound line 95
  12. theorem OAI.SignedSweeps.rightHookProduct_le line 123