OAI/NumberTheory/Catalan/Arithmetic/OddPrimeUpperPoolEnumeration.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.oddPrimeUpperPairHighSet line 9
  2. def OAI.InternalCatalan.oddPrimeUpperCentralSet line 12
  3. def OAI.InternalCatalan.oddPrimeUpperRetainedSet line 15
  4. def OAI.InternalCatalan.oddPrimeUpperExceptionalSet line 19
  5. theorem OAI.InternalCatalan.oddPrimeUpperPairHighSet_mem_iff line 22
  6. theorem OAI.InternalCatalan.oddPrimeUpperCentralSet_mem_iff line 32
  7. theorem OAI.InternalCatalan.oddPrimeUpperPairHighSet_subset_raw line 38
  8. theorem OAI.InternalCatalan.oddPrimeUpperCentralSet_subset_raw line 45
  9. theorem OAI.InternalCatalan.oddPrimeUpperRetainedSet_subset_raw line 51
  10. theorem OAI.InternalCatalan.oddPrimeUpperPairHighSet_disjoint_central line 56
  11. theorem OAI.InternalCatalan.oddPrimeUpperRetainedSet_disjoint_pairHigh line 64
  12. theorem OAI.InternalCatalan.oddPrimeUpperRetainedSet_disjoint_central line 70
  13. theorem OAI.InternalCatalan.oddPrimeUpperPool_partition line 76
  14. theorem OAI.InternalCatalan.oddPrimeUpperRetainedSet_mem_iff line 94
  15. theorem OAI.InternalCatalan.oddPrimeUpperPairHighSet_card line 121
  16. theorem OAI.InternalCatalan.oddPrimeUpperCentralSet_card line 126
  17. theorem OAI.InternalCatalan.oddPrimeUpperRetainedSet_card line 130
  18. theorem OAI.InternalCatalan.oddPrimeUpperExceptionalSet_card line 145
  19. theorem OAI.InternalCatalan.oddPrimeUpperExceptionalSet_mem_iff line 149
  20. theorem OAI.InternalCatalan.oddPrimeUpperPairIndex_bounds line 155
  21. def OAI.InternalCatalan.rawColumnPoolEquiv line 188
  22. theorem OAI.InternalCatalan.rawColumnPoolEquiv_apply_val line 208
  23. theorem OAI.InternalCatalan.rawColumnPoolEquiv_symm_apply_val line 211
  24. def OAI.InternalCatalan.oddPrimeUpperPoolSplit line 215
  25. def OAI.InternalCatalan.oddPrimeUpperPoolEnumeration line 272
  26. theorem OAI.InternalCatalan.oddPrimeUpperPoolEnumeration_retained_val line 282
  27. theorem OAI.InternalCatalan.oddPrimeUpperPoolEnumeration_pairHigh_val line 287
  28. theorem OAI.InternalCatalan.oddPrimeUpperPoolEnumeration_central_val line 292