OAI/NumberTheory/Catalan/Arithmetic/FinitePlaceAssembly.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.momentStartingRat line 17
  2. theorem OAI.InternalCatalan.momentRat_reverse_diagonal line 20
  3. theorem OAI.InternalCatalan.momentScalarPred_central_reduction line 53
  4. theorem OAI.InternalCatalan.momentStartingRat_central_den_ne_zero line 81
  5. theorem OAI.InternalCatalan.momentScalarPred_central_div_reduction line 102
  6. theorem OAI.InternalCatalan.momentRat_central_reduction line 142
  7. theorem OAI.InternalCatalan.oddPrime_central_strip_range line 195
  8. theorem OAI.InternalCatalan.rowP_momentRat_central_reduction line 217
  9. def OAI.InternalCatalan.oddPrimeLeadingV line 306
  10. theorem OAI.InternalCatalan.rawCatalanTerm_prime_reduction line 310
  11. theorem OAI.InternalCatalan.rawEntryRat_central_layer line 323
  12. theorem OAI.InternalCatalan.rawEntryRat_low_leading line 385
  13. theorem OAI.InternalCatalan.rawEntryRat_high_leading line 432
  14. def OAI.InternalCatalan.oddPrimeRepresented line 467
  15. instance OAI.InternalCatalan.oddPrimeRepresented_decidable line 470
  16. def OAI.InternalCatalan.oddPrimeRepresentativeRat line 473
  17. theorem OAI.InternalCatalan.oddPrimeRepresentativeRat_scaled_reduction line 476
  18. def OAI.InternalCatalan.oddPrimeShearedRat line 511
  19. theorem OAI.InternalCatalan.oddPrimeShearedRat_scaled_reduction line 519
  20. def OAI.InternalCatalan.oddPrimeLeadingLiftRat line 623
  21. def OAI.InternalCatalan.oddPrimeExceptionalPartRat line 626
  22. def OAI.InternalCatalan.oddPrimeCentralRemainderRat line 632
  23. theorem OAI.InternalCatalan.oddPrimeLeadingLiftRat_reduction line 635
  24. theorem OAI.InternalCatalan.oddPrimeExceptionalPartRat_reduction line 641
  25. theorem OAI.InternalCatalan.oddPrimeCentralRemainderRat_den_ne_zero line 696
  26. theorem OAI.InternalCatalan.oddPrimeShearedRat_eq_remainder_add_exceptional line 706
  27. def OAI.InternalCatalan.oddPrimeUpperPairIndex line 725
  28. def OAI.InternalCatalan.oddPrimeUpperCentralIndex line 728
  29. instance OAI.InternalCatalan.oddPrimeUpperPairIndex_decidable line 731
  30. instance OAI.InternalCatalan.oddPrimeUpperCentralIndex_decidable line 735
  31. def OAI.InternalCatalan.oddPrimeUpperPoolRat line 739
  32. def OAI.InternalCatalan.oddPrimeUpperRepresentativePoolRat line 745
  33. theorem OAI.InternalCatalan.oddPrimeUpperPoolRat_pair_low line 749
  34. theorem OAI.InternalCatalan.oddPrimeUpperRepresentativePoolRat_eq line 766
  35. theorem OAI.InternalCatalan.rawEntryRat_eq_upper_pool_inverse line 789
  36. abbrev OAI.InternalCatalan.oddPrimeUpperExceptionalSize line 836
  37. theorem OAI.InternalCatalan.oddPrimeUpperExceptional_sum_eq line 839
  38. theorem OAI.InternalCatalan.oddPrimeUpperExceptional_combination_eq line 863
  39. abbrev OAI.InternalCatalan.oddPrimeUpperRetainedSize line 893
  40. abbrev OAI.InternalCatalan.oddPrimeUpperPairedSize line 894
  41. abbrev OAI.InternalCatalan.oddPrimeUpperCentralSize line 895
  42. abbrev OAI.InternalCatalan.oddPrimeUpperPhysicalIndex line 896
  43. def OAI.InternalCatalan.oddPrimeUpperRetainedVector line 900
  44. def OAI.InternalCatalan.oddPrimeUpperPairedVector line 905
  45. def OAI.InternalCatalan.oddPrimeUpperIntegralVector line 910
  46. def OAI.InternalCatalan.oddPrimeUpperExceptionalVector line 915
  47. def OAI.InternalCatalan.oddPrimeUpperExceptionalCoeff line 920
  48. def OAI.InternalCatalan.oddPrimeUpperPhysicalColumn line 927
  49. theorem OAI.InternalCatalan.oddPrimeUpperRetainedVector_den_ne_zero line 933
  50. theorem OAI.InternalCatalan.oddPrimeUpperPairedVector_den_ne_zero line 943
  51. theorem OAI.InternalCatalan.oddPrimeUpperIntegralVector_den_ne_zero line 964
  52. theorem OAI.InternalCatalan.oddPrimeUpperExceptionalVector_den_ne_zero line 974
  53. theorem OAI.InternalCatalan.oddPrimeUpperExceptionalCoeff_den_ne_zero line 980
  54. theorem OAI.InternalCatalan.oddPrimeUpperExceptionalVector_combination line 998
  55. theorem OAI.InternalCatalan.oddPrimeUpperPhysicalColumn_eq_pool line 1008
  56. def OAI.InternalCatalan.oddPrimeUpperDelta line 1072
  57. def OAI.InternalCatalan.oddPrimeUpperRepresentativeNumber line 1076
  58. def OAI.InternalCatalan.oddPrimeUpperRepresentativeSign line 1079
  59. def OAI.InternalCatalan.oddPrimeUpperShearCoeff line 1082
  60. def OAI.InternalCatalan.oddPrimeUpperInverseCoeff line 1089
  61. theorem OAI.InternalCatalan.upper_delta_den_ne_zero line 1109
  62. theorem OAI.InternalCatalan.upper_sign_den_ne_zero line 1115
  63. theorem OAI.InternalCatalan.upper_shearCoeff_den_ne_zero line 1120
  64. theorem OAI.InternalCatalan.oddPrimeUpperInverseCoeff_den_ne_zero line 1150
  65. theorem OAI.InternalCatalan.oddPrimeUpperDelta_sum line 1184
  66. theorem OAI.InternalCatalan.oddPrimeUpperRepresentativeNumber_mem line 1206
  67. theorem OAI.InternalCatalan.oddPrimeUpperRepresentativePoolRat_eq_sign line 1220
  68. theorem OAI.InternalCatalan.oddPrimeUpperShearCoeff_sum line 1228
  69. theorem OAI.InternalCatalan.rawEntryRat_eq_upper_physical_sum line 1254
  70. theorem OAI.InternalCatalan.oddPrimeUpperPhysical_loss_eq line 1328
  71. theorem OAI.InternalCatalan.oddPrimeUpperPhysicalCombination_valuation_lower line 1344
  72. theorem OAI.InternalCatalan.rawMinorRat_odd_upper_valuation line 1366
  73. theorem OAI.InternalCatalan.determinantRat_odd_upper_valuation line 1382
  74. theorem OAI.InternalCatalan.determinantRat_odd_prime_loss_upper line 1395
  75. theorem OAI.InternalCatalan.determinantRat_odd_prime_large_loss_lower line 1417
  76. theorem OAI.InternalCatalan.largeOddPrimeContribution_eventually_lower line 1432
  77. theorem OAI.InternalCatalan.determinantRat_finite_place_eventually_lower line 1482
  78. theorem OAI.InternalCatalan.determinantRat_finite_place_threshold line 1495