OAI/Probability/SwitchChain/CrossMatrix.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem315.CrossBlock.Matrix line 9
  2. def OAI.Problem315.CrossBlock.entry line 11
  3. def OAI.Problem315.CrossBlock.row line 13
  4. def OAI.Problem315.CrossBlock.col line 15
  5. def OAI.Problem315.CrossBlock.total line 17
  6. def OAI.Problem315.CrossBlock.count line 19
  7. theorem OAI.Problem315.CrossBlock.count_two line 22
  8. theorem OAI.Problem315.CrossBlock.count_one line 26
  9. theorem OAI.Problem315.CrossBlock.count_three line 30
  10. theorem OAI.Problem315.CrossBlock.count_zero line 34
  11. theorem OAI.Problem315.CrossBlock.count_four line 38
  12. theorem OAI.Problem315.CrossBlock.off_center_disjoint line 42
  13. theorem OAI.Problem315.CrossBlock.central_iff line 46
  14. def OAI.Problem315.CrossBlock.toggle line 51
  15. theorem OAI.Problem315.CrossBlock.toggle_involutive line 56
  16. theorem OAI.Problem315.CrossBlock.toggle_row line 59
  17. theorem OAI.Problem315.CrossBlock.toggle_col line 62
  18. theorem OAI.Problem315.CrossBlock.toggle_total line 65
  19. theorem OAI.Problem315.CrossBlock.toggle_ne_iff line 68
  20. theorem OAI.Problem315.CrossBlock.row_le_two line 72
  21. theorem OAI.Problem315.CrossBlock.col_le_two line 75
  22. theorem OAI.Problem315.CrossBlock.total_le_four line 78
  23. theorem OAI.Problem315.CrossBlock.count_two_real line 81