OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairPattern.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.HistoryPairPattern.PairKey line 10
  2. instance OAI.Ostmann.Arithmetic.HistoryPairPattern.pairKeyDecidableEq line 14
  3. instance OAI.Ostmann.Arithmetic.HistoryPairPattern.pairKeyFintype line 18
  4. def OAI.Ostmann.Arithmetic.HistoryPairPattern.leftEmbedding line 22
  5. def OAI.Ostmann.Arithmetic.HistoryPairPattern.rightEmbedding line 29
  6. def OAI.Ostmann.Arithmetic.HistoryPairPattern.leftMap line 36
  7. def OAI.Ostmann.Arithmetic.HistoryPairPattern.rightMap line 39
  8. def OAI.Ostmann.Arithmetic.HistoryPairPattern.unionMap line 42
  9. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.unionMap_surjective line 45
  10. def OAI.Ostmann.Arithmetic.HistoryPairPattern.pairSample line 53
  11. def OAI.Ostmann.Arithmetic.HistoryPairPattern.pairRationalSample line 55
  12. def OAI.Ostmann.Arithmetic.HistoryPairPattern.pairLevel line 57
  13. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.leftMap_sample line 59
  14. def OAI.Ostmann.Arithmetic.HistoryPairPattern.RootGiantsAgree line 62
  15. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.RootGiantsAgree.of_root_eq line 65
  16. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.rightMap_sample line 69
  17. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.leftEmbedding_sample line 77
  18. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.rightEmbedding_sample line 80
  19. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.leftMap_level line 85
  20. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.rightMap_level line 88
  21. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.leftEmbedding_level line 91
  22. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.rightEmbedding_level line 94
  23. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.shared_giant line 97
  24. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.cross_small_eq_iff line 100
  25. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.left_giant_ne_right_small line 108
  26. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.leftSmall_ne_right_giant line 115
  27. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.leftEmbedding_injective line 122
  28. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.rightEmbedding_injective line 125
  29. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.leftMap_sample_comp line 128
  30. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.rightMap_sample_comp line 133
  31. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.leftMap_rational_comp line 138
  32. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.rightMap_rational_comp line 143
  33. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.leftMap_cast_comp line 148
  34. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.rightMap_cast_comp line 153
  35. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.left_integerEval line 159
  36. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.right_integerEval line 163
  37. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.left_rationalEval line 167
  38. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.right_rationalEval line 171
  39. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.left_fieldEval line 175
  40. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.right_fieldEval line 180
  41. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.left_regularAt line 186
  42. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.right_regularAt line 190
  43. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.left_fieldRegularAt line 194
  44. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.right_fieldRegularAt line 199
  45. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.left_above line 205
  46. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.right_above line 209
  47. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.leftEmbedding_above line 213
  48. theorem OAI.Ostmann.Arithmetic.HistoryPairPattern.rightEmbedding_above line 218