OAI/NumberTheory/Catalan/Determinants/ManuscriptNormRoundingPRow01.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.manuscriptNormP1_0SubstituteRat line 15
  2. theorem OAI.InternalCatalan.manuscriptNormP1_0SubstituteRat_interval line 18
  3. theorem OAI.InternalCatalan.manuscriptNormP1_0SubstituteRat_upper line 23
  4. def OAI.InternalCatalan.manuscriptNormP1_1SubstituteRat line 27
  5. theorem OAI.InternalCatalan.manuscriptNormP1_1SubstituteRat_interval line 30
  6. theorem OAI.InternalCatalan.manuscriptNormP1_1SubstituteRat_upper line 35
  7. def OAI.InternalCatalan.manuscriptNormP1_2SubstituteRat line 39
  8. theorem OAI.InternalCatalan.manuscriptNormP1_2SubstituteRat_interval line 42
  9. theorem OAI.InternalCatalan.manuscriptNormP1_2SubstituteRat_upper line 47
  10. def OAI.InternalCatalan.manuscriptNormP1_3SubstituteRat line 51
  11. theorem OAI.InternalCatalan.manuscriptNormP1_3SubstituteRat_interval line 54
  12. theorem OAI.InternalCatalan.manuscriptNormP1_3SubstituteRat_upper line 59
  13. def OAI.InternalCatalan.manuscriptNormP1_4SubstituteRat line 63
  14. theorem OAI.InternalCatalan.manuscriptNormP1_4SubstituteRat_interval line 66
  15. theorem OAI.InternalCatalan.manuscriptNormP1_4SubstituteRat_upper line 71
  16. def OAI.InternalCatalan.manuscriptNormP1_5SubstituteRat line 75
  17. theorem OAI.InternalCatalan.manuscriptNormP1_5SubstituteRat_interval line 78
  18. theorem OAI.InternalCatalan.manuscriptNormP1_5SubstituteRat_upper line 83
  19. def OAI.InternalCatalan.manuscriptNormP1_6SubstituteRat line 87
  20. theorem OAI.InternalCatalan.manuscriptNormP1_6SubstituteRat_interval line 90
  21. theorem OAI.InternalCatalan.manuscriptNormP1_6SubstituteRat_upper line 95
  22. def OAI.InternalCatalan.manuscriptNormP1_7SubstituteRat line 99
  23. theorem OAI.InternalCatalan.manuscriptNormP1_7SubstituteRat_interval line 102
  24. theorem OAI.InternalCatalan.manuscriptNormP1_7SubstituteRat_upper line 107
  25. def OAI.InternalCatalan.manuscriptNormP1_8SubstituteRat line 111
  26. theorem OAI.InternalCatalan.manuscriptNormP1_8SubstituteRat_interval line 114
  27. theorem OAI.InternalCatalan.manuscriptNormP1_8SubstituteRat_upper line 119
  28. def OAI.InternalCatalan.manuscriptNormP1_9SubstituteRat line 123
  29. theorem OAI.InternalCatalan.manuscriptNormP1_9SubstituteRat_interval line 126
  30. theorem OAI.InternalCatalan.manuscriptNormP1_9SubstituteRat_upper line 131
  31. def OAI.InternalCatalan.manuscriptNormPSubstituteRow1 line 135
  32. theorem OAI.InternalCatalan.manuscriptNormPSubstituteRow1_upper line 147
  33. theorem OAI.InternalCatalan.manuscriptNormP1_0SubstituteRat_composition_error line 170
  34. theorem OAI.InternalCatalan.manuscriptNormP1_1SubstituteRat_composition_error line 182
  35. theorem OAI.InternalCatalan.manuscriptNormP1_2SubstituteRat_composition_error line 194
  36. theorem OAI.InternalCatalan.manuscriptNormP1_3SubstituteRat_composition_error line 206
  37. theorem OAI.InternalCatalan.manuscriptNormP1_4SubstituteRat_composition_error line 218
  38. theorem OAI.InternalCatalan.manuscriptNormP1_5SubstituteRat_composition_error line 230
  39. theorem OAI.InternalCatalan.manuscriptNormP1_6SubstituteRat_composition_error line 242
  40. theorem OAI.InternalCatalan.manuscriptNormP1_7SubstituteRat_composition_error line 254
  41. theorem OAI.InternalCatalan.manuscriptNormP1_8SubstituteRat_composition_error line 266
  42. theorem OAI.InternalCatalan.manuscriptNormP1_9SubstituteRat_composition_error line 278
  43. theorem OAI.InternalCatalan.manuscriptNormPCompositionRow1_error line 290
  44. def OAI.InternalCatalan.manuscriptNormP1_0RoundedSubstituteRat line 340
  45. theorem OAI.InternalCatalan.manuscriptNormP1_0RoundedSubstituteRat_error line 343
  46. def OAI.InternalCatalan.manuscriptNormP1_1RoundedSubstituteRat line 353
  47. theorem OAI.InternalCatalan.manuscriptNormP1_1RoundedSubstituteRat_error line 356
  48. def OAI.InternalCatalan.manuscriptNormP1_2RoundedSubstituteRat line 366
  49. theorem OAI.InternalCatalan.manuscriptNormP1_2RoundedSubstituteRat_error line 369
  50. def OAI.InternalCatalan.manuscriptNormP1_3RoundedSubstituteRat line 379
  51. theorem OAI.InternalCatalan.manuscriptNormP1_3RoundedSubstituteRat_error line 382
  52. def OAI.InternalCatalan.manuscriptNormP1_4RoundedSubstituteRat line 392
  53. theorem OAI.InternalCatalan.manuscriptNormP1_4RoundedSubstituteRat_error line 395
  54. def OAI.InternalCatalan.manuscriptNormP1_5RoundedSubstituteRat line 405
  55. theorem OAI.InternalCatalan.manuscriptNormP1_5RoundedSubstituteRat_error line 408
  56. def OAI.InternalCatalan.manuscriptNormP1_6RoundedSubstituteRat line 418
  57. theorem OAI.InternalCatalan.manuscriptNormP1_6RoundedSubstituteRat_error line 421
  58. def OAI.InternalCatalan.manuscriptNormP1_7RoundedSubstituteRat line 431
  59. theorem OAI.InternalCatalan.manuscriptNormP1_7RoundedSubstituteRat_error line 434
  60. def OAI.InternalCatalan.manuscriptNormP1_8RoundedSubstituteRat line 444
  61. theorem OAI.InternalCatalan.manuscriptNormP1_8RoundedSubstituteRat_error line 447
  62. def OAI.InternalCatalan.manuscriptNormP1_9RoundedSubstituteRat line 457
  63. theorem OAI.InternalCatalan.manuscriptNormP1_9RoundedSubstituteRat_error line 460
  64. def OAI.InternalCatalan.manuscriptNormPRoundedSubstituteRow1 line 470
  65. theorem OAI.InternalCatalan.manuscriptNormPRoundedRow1_error line 482