OAI/Geometry/HeilbronnTriangle/CRTLifting.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem355.CRT.ResidueLift line 8
  2. def OAI.Problem355.CRT.residueLiftEquiv line 10
  3. theorem OAI.Problem355.CRT.card_residueLift line 31
  4. abbrev OAI.Problem355.CRT.DoubleResidueLift line 35
  5. def OAI.Problem355.CRT.crtRepresentative line 38
  6. theorem OAI.Problem355.CRT.doubleResidue_iff line 41
  7. def OAI.Problem355.CRT.doubleResidueLiftEquiv line 65
  8. theorem OAI.Problem355.CRT.card_doubleResidueLift line 73
  9. abbrev OAI.Problem355.CRT.ResidueBox line 78
  10. theorem OAI.Problem355.CRT.card_residueBox line 82
  11. theorem OAI.Problem355.CRT.card_column_lifts line 97
  12. theorem OAI.Problem355.CRT.translate_box_length line 103
  13. def OAI.Problem355.CRT.intervalEquiv line 108
  14. abbrev OAI.Problem355.CRT.IntegerDoubleResidueLift line 122
  15. def OAI.Problem355.CRT.integerDoubleResidueLiftEquiv line 126
  16. theorem OAI.Problem355.CRT.card_integerDoubleResidueLift line 137
  17. abbrev OAI.Problem355.CRT.IntegerResidueBox line 144
  18. theorem OAI.Problem355.CRT.card_integerResidueBox line 147
  19. def OAI.Problem355.CRT.integerBoxColumn line 156
  20. theorem OAI.Problem355.CRT.integerBoxColumn_injective line 160
  21. def OAI.Problem355.CRT.integerColumnLifts line 168
  22. theorem OAI.Problem355.CRT.mem_integerColumnLifts_iff line 173
  23. theorem OAI.Problem355.CRT.card_integerColumnLifts line 185
  24. def OAI.Problem355.CRT.zmodResidueLiftEquiv line 201
  25. theorem OAI.Problem355.CRT.card_residue_lifts line 221
  26. theorem OAI.Problem355.CRT.crt_residue_iff line 225
  27. def OAI.Problem355.CRT.crtLiftEquiv line 237
  28. theorem OAI.Problem355.CRT.card_crt_lifts line 244
  29. def OAI.Problem355.CRT.crtVectorLiftEquiv line 250
  30. theorem OAI.Problem355.CRT.card_crt_vector_lifts line 258
  31. def OAI.Problem355.CRT.intIntervalEquiv line 265
  32. def OAI.Problem355.CRT.intCRTLiftEquiv line 283
  33. theorem OAI.Problem355.CRT.card_int_crt_lifts line 300
  34. def OAI.Problem355.CRT.intCRTVectorLiftEquiv line 306
  35. theorem OAI.Problem355.CRT.card_int_crt_vector_lifts line 315
  36. theorem OAI.Problem355.CRT.card_int_crt_vector_lifts_of_dvd line 324
  37. theorem OAI.Problem355.CRT.int_crt_vector_lifts_nonempty line 336