OAI/NumberTheory/Catalan/Determinants/ManuscriptNormRoundingPRow04.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.manuscriptNormP4_0SubstituteRat line 15
  2. theorem OAI.InternalCatalan.manuscriptNormP4_0SubstituteRat_interval line 18
  3. theorem OAI.InternalCatalan.manuscriptNormP4_0SubstituteRat_upper line 23
  4. def OAI.InternalCatalan.manuscriptNormP4_1SubstituteRat line 27
  5. theorem OAI.InternalCatalan.manuscriptNormP4_1SubstituteRat_interval line 30
  6. theorem OAI.InternalCatalan.manuscriptNormP4_1SubstituteRat_upper line 35
  7. def OAI.InternalCatalan.manuscriptNormP4_2SubstituteRat line 39
  8. theorem OAI.InternalCatalan.manuscriptNormP4_2SubstituteRat_interval line 42
  9. theorem OAI.InternalCatalan.manuscriptNormP4_2SubstituteRat_upper line 47
  10. def OAI.InternalCatalan.manuscriptNormP4_3SubstituteRat line 51
  11. theorem OAI.InternalCatalan.manuscriptNormP4_3SubstituteRat_interval line 54
  12. theorem OAI.InternalCatalan.manuscriptNormP4_3SubstituteRat_upper line 59
  13. def OAI.InternalCatalan.manuscriptNormP4_4SubstituteRat line 63
  14. theorem OAI.InternalCatalan.manuscriptNormP4_4SubstituteRat_interval line 66
  15. theorem OAI.InternalCatalan.manuscriptNormP4_4SubstituteRat_upper line 71
  16. def OAI.InternalCatalan.manuscriptNormP4_5SubstituteRat line 75
  17. theorem OAI.InternalCatalan.manuscriptNormP4_5SubstituteRat_interval line 78
  18. theorem OAI.InternalCatalan.manuscriptNormP4_5SubstituteRat_upper line 83
  19. def OAI.InternalCatalan.manuscriptNormP4_6SubstituteRat line 87
  20. theorem OAI.InternalCatalan.manuscriptNormP4_6SubstituteRat_interval line 90
  21. theorem OAI.InternalCatalan.manuscriptNormP4_6SubstituteRat_upper line 95
  22. def OAI.InternalCatalan.manuscriptNormP4_7SubstituteRat line 99
  23. theorem OAI.InternalCatalan.manuscriptNormP4_7SubstituteRat_interval line 102
  24. theorem OAI.InternalCatalan.manuscriptNormP4_7SubstituteRat_upper line 107
  25. def OAI.InternalCatalan.manuscriptNormP4_8SubstituteRat line 111
  26. theorem OAI.InternalCatalan.manuscriptNormP4_8SubstituteRat_interval line 114
  27. theorem OAI.InternalCatalan.manuscriptNormP4_8SubstituteRat_upper line 119
  28. def OAI.InternalCatalan.manuscriptNormP4_9SubstituteRat line 123
  29. theorem OAI.InternalCatalan.manuscriptNormP4_9SubstituteRat_interval line 126
  30. theorem OAI.InternalCatalan.manuscriptNormP4_9SubstituteRat_upper line 131
  31. def OAI.InternalCatalan.manuscriptNormPSubstituteRow4 line 135
  32. theorem OAI.InternalCatalan.manuscriptNormPSubstituteRow4_upper line 147
  33. theorem OAI.InternalCatalan.manuscriptNormP4_0SubstituteRat_composition_error line 170
  34. theorem OAI.InternalCatalan.manuscriptNormP4_1SubstituteRat_composition_error line 182
  35. theorem OAI.InternalCatalan.manuscriptNormP4_2SubstituteRat_composition_error line 194
  36. theorem OAI.InternalCatalan.manuscriptNormP4_3SubstituteRat_composition_error line 206
  37. theorem OAI.InternalCatalan.manuscriptNormP4_4SubstituteRat_composition_error line 218
  38. theorem OAI.InternalCatalan.manuscriptNormP4_5SubstituteRat_composition_error line 230
  39. theorem OAI.InternalCatalan.manuscriptNormP4_6SubstituteRat_composition_error line 242
  40. theorem OAI.InternalCatalan.manuscriptNormP4_7SubstituteRat_composition_error line 254
  41. theorem OAI.InternalCatalan.manuscriptNormP4_8SubstituteRat_composition_error line 266
  42. theorem OAI.InternalCatalan.manuscriptNormP4_9SubstituteRat_composition_error line 278
  43. theorem OAI.InternalCatalan.manuscriptNormPCompositionRow4_error line 290
  44. def OAI.InternalCatalan.manuscriptNormP4_0RoundedSubstituteRat line 340
  45. theorem OAI.InternalCatalan.manuscriptNormP4_0RoundedSubstituteRat_error line 343
  46. def OAI.InternalCatalan.manuscriptNormP4_1RoundedSubstituteRat line 353
  47. theorem OAI.InternalCatalan.manuscriptNormP4_1RoundedSubstituteRat_error line 356
  48. def OAI.InternalCatalan.manuscriptNormP4_2RoundedSubstituteRat line 366
  49. theorem OAI.InternalCatalan.manuscriptNormP4_2RoundedSubstituteRat_error line 369
  50. def OAI.InternalCatalan.manuscriptNormP4_3RoundedSubstituteRat line 379
  51. theorem OAI.InternalCatalan.manuscriptNormP4_3RoundedSubstituteRat_error line 382
  52. def OAI.InternalCatalan.manuscriptNormP4_4RoundedSubstituteRat line 392
  53. theorem OAI.InternalCatalan.manuscriptNormP4_4RoundedSubstituteRat_error line 395
  54. def OAI.InternalCatalan.manuscriptNormP4_5RoundedSubstituteRat line 405
  55. theorem OAI.InternalCatalan.manuscriptNormP4_5RoundedSubstituteRat_error line 408
  56. def OAI.InternalCatalan.manuscriptNormP4_6RoundedSubstituteRat line 418
  57. theorem OAI.InternalCatalan.manuscriptNormP4_6RoundedSubstituteRat_error line 421
  58. def OAI.InternalCatalan.manuscriptNormP4_7RoundedSubstituteRat line 431
  59. theorem OAI.InternalCatalan.manuscriptNormP4_7RoundedSubstituteRat_error line 434
  60. def OAI.InternalCatalan.manuscriptNormP4_8RoundedSubstituteRat line 444
  61. theorem OAI.InternalCatalan.manuscriptNormP4_8RoundedSubstituteRat_error line 447
  62. def OAI.InternalCatalan.manuscriptNormP4_9RoundedSubstituteRat line 457
  63. theorem OAI.InternalCatalan.manuscriptNormP4_9RoundedSubstituteRat_error line 460
  64. def OAI.InternalCatalan.manuscriptNormPRoundedSubstituteRow4 line 470
  65. theorem OAI.InternalCatalan.manuscriptNormPRoundedRow4_error line 482