OAI/Combinatorics/CompleteCrossing/Residues.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Residue fibers, same-page residues, and parity counts.

  1. theorem OAI.Paper170.sameColorResidues_eq_intervals line 15
  2. theorem OAI.Paper170.sameColorResidues_eq_intervals_large line 32
  3. theorem OAI.Paper170.sameColorResidues_card line 49
  4. theorem OAI.Paper170.residueColor_mod line 70
  5. theorem OAI.Paper170.residueColor_add_half line 73
  6. theorem OAI.Paper170.sameColorResidues_half_shift line 85
  7. theorem OAI.Paper170.residueFiber_card_odd line 106
  8. theorem OAI.Paper170.add_mod_inj line 129
  9. theorem OAI.Paper170.add_mod_surj line 134
  10. theorem OAI.Paper170.doubled_residue line 143
  11. theorem OAI.Paper170.residueFiber_card_even line 154
  12. theorem OAI.Paper170.parity_balance_of_involution line 197
  13. theorem OAI.Paper170.interval_parity_balance line 214
  14. theorem OAI.Paper170.firstGapParity_balance line 233
  15. theorem OAI.Paper170.parity_balance_union line 246
  16. theorem OAI.Paper170.sameColorResidues_parity_balance line 256