OAI/NumberTheory/Catalan/Determinants/ManuscriptNormRoundingPRow00.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.manuscriptNormP0_0SubstituteRat line 13
  2. theorem OAI.InternalCatalan.manuscriptNormP0_0SubstituteRat_interval line 16
  3. theorem OAI.InternalCatalan.manuscriptNormP0_0SubstituteRat_upper line 21
  4. def OAI.InternalCatalan.manuscriptNormP0_1SubstituteRat line 25
  5. theorem OAI.InternalCatalan.manuscriptNormP0_1SubstituteRat_interval line 28
  6. theorem OAI.InternalCatalan.manuscriptNormP0_1SubstituteRat_upper line 33
  7. def OAI.InternalCatalan.manuscriptNormP0_2SubstituteRat line 37
  8. theorem OAI.InternalCatalan.manuscriptNormP0_2SubstituteRat_interval line 40
  9. theorem OAI.InternalCatalan.manuscriptNormP0_2SubstituteRat_upper line 45
  10. def OAI.InternalCatalan.manuscriptNormP0_3SubstituteRat line 49
  11. theorem OAI.InternalCatalan.manuscriptNormP0_3SubstituteRat_interval line 52
  12. theorem OAI.InternalCatalan.manuscriptNormP0_3SubstituteRat_upper line 57
  13. def OAI.InternalCatalan.manuscriptNormP0_4SubstituteRat line 61
  14. theorem OAI.InternalCatalan.manuscriptNormP0_4SubstituteRat_interval line 64
  15. theorem OAI.InternalCatalan.manuscriptNormP0_4SubstituteRat_upper line 69
  16. def OAI.InternalCatalan.manuscriptNormP0_5SubstituteRat line 73
  17. theorem OAI.InternalCatalan.manuscriptNormP0_5SubstituteRat_interval line 76
  18. theorem OAI.InternalCatalan.manuscriptNormP0_5SubstituteRat_upper line 81
  19. def OAI.InternalCatalan.manuscriptNormP0_6SubstituteRat line 85
  20. theorem OAI.InternalCatalan.manuscriptNormP0_6SubstituteRat_interval line 88
  21. theorem OAI.InternalCatalan.manuscriptNormP0_6SubstituteRat_upper line 93
  22. def OAI.InternalCatalan.manuscriptNormP0_7SubstituteRat line 97
  23. theorem OAI.InternalCatalan.manuscriptNormP0_7SubstituteRat_interval line 100
  24. theorem OAI.InternalCatalan.manuscriptNormP0_7SubstituteRat_upper line 105
  25. def OAI.InternalCatalan.manuscriptNormP0_8SubstituteRat line 109
  26. theorem OAI.InternalCatalan.manuscriptNormP0_8SubstituteRat_interval line 112
  27. theorem OAI.InternalCatalan.manuscriptNormP0_8SubstituteRat_upper line 117
  28. def OAI.InternalCatalan.manuscriptNormP0_9SubstituteRat line 121
  29. theorem OAI.InternalCatalan.manuscriptNormP0_9SubstituteRat_interval line 124
  30. theorem OAI.InternalCatalan.manuscriptNormP0_9SubstituteRat_upper line 129
  31. def OAI.InternalCatalan.manuscriptNormPSubstituteRow0 line 133
  32. theorem OAI.InternalCatalan.manuscriptNormPSubstituteRow0_upper line 145
  33. theorem OAI.InternalCatalan.manuscriptNormP0_0SubstituteRat_composition_error line 168
  34. theorem OAI.InternalCatalan.manuscriptNormP0_1SubstituteRat_composition_error line 180
  35. theorem OAI.InternalCatalan.manuscriptNormP0_2SubstituteRat_composition_error line 192
  36. theorem OAI.InternalCatalan.manuscriptNormP0_3SubstituteRat_composition_error line 204
  37. theorem OAI.InternalCatalan.manuscriptNormP0_4SubstituteRat_composition_error line 216
  38. theorem OAI.InternalCatalan.manuscriptNormP0_5SubstituteRat_composition_error line 228
  39. theorem OAI.InternalCatalan.manuscriptNormP0_6SubstituteRat_composition_error line 240
  40. theorem OAI.InternalCatalan.manuscriptNormP0_7SubstituteRat_composition_error line 252
  41. theorem OAI.InternalCatalan.manuscriptNormP0_8SubstituteRat_composition_error line 264
  42. theorem OAI.InternalCatalan.manuscriptNormP0_9SubstituteRat_composition_error line 276
  43. theorem OAI.InternalCatalan.manuscriptNormPCompositionRow0_error line 288
  44. def OAI.InternalCatalan.manuscriptNormP0_0RoundedSubstituteRat line 338
  45. theorem OAI.InternalCatalan.manuscriptNormP0_0RoundedSubstituteRat_error line 341
  46. def OAI.InternalCatalan.manuscriptNormP0_1RoundedSubstituteRat line 351
  47. theorem OAI.InternalCatalan.manuscriptNormP0_1RoundedSubstituteRat_error line 354
  48. def OAI.InternalCatalan.manuscriptNormP0_2RoundedSubstituteRat line 364
  49. theorem OAI.InternalCatalan.manuscriptNormP0_2RoundedSubstituteRat_error line 367
  50. def OAI.InternalCatalan.manuscriptNormP0_3RoundedSubstituteRat line 377
  51. theorem OAI.InternalCatalan.manuscriptNormP0_3RoundedSubstituteRat_error line 380
  52. def OAI.InternalCatalan.manuscriptNormP0_4RoundedSubstituteRat line 390
  53. theorem OAI.InternalCatalan.manuscriptNormP0_4RoundedSubstituteRat_error line 393
  54. def OAI.InternalCatalan.manuscriptNormP0_5RoundedSubstituteRat line 403
  55. theorem OAI.InternalCatalan.manuscriptNormP0_5RoundedSubstituteRat_error line 406
  56. def OAI.InternalCatalan.manuscriptNormP0_6RoundedSubstituteRat line 416
  57. theorem OAI.InternalCatalan.manuscriptNormP0_6RoundedSubstituteRat_error line 419
  58. def OAI.InternalCatalan.manuscriptNormP0_7RoundedSubstituteRat line 429
  59. theorem OAI.InternalCatalan.manuscriptNormP0_7RoundedSubstituteRat_error line 432
  60. def OAI.InternalCatalan.manuscriptNormP0_8RoundedSubstituteRat line 442
  61. theorem OAI.InternalCatalan.manuscriptNormP0_8RoundedSubstituteRat_error line 445
  62. def OAI.InternalCatalan.manuscriptNormP0_9RoundedSubstituteRat line 455
  63. theorem OAI.InternalCatalan.manuscriptNormP0_9RoundedSubstituteRat_error line 458
  64. def OAI.InternalCatalan.manuscriptNormPRoundedSubstituteRow0 line 468
  65. theorem OAI.InternalCatalan.manuscriptNormPRoundedRow0_error line 480