OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoDescartesY2.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_20 line 12
  2. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_21 line 16
  3. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_22 line 20
  4. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_23 line 24
  5. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_24 line 28
  6. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_20 line 32
  7. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_21 line 40
  8. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_22 line 48
  9. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_23 line 56
  10. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_24 line 64
  11. theorem OAI.InternalCatalan.barrierCase2AY_transform2_all_coeff_rat line 72
  12. theorem OAI.InternalCatalan.barrierCase2AYTransform2Explicit_coeff line 105
  13. theorem OAI.InternalCatalan.barrierCase2AY_transform2_eq_explicit line 135
  14. theorem OAI.InternalCatalan.barrierCase2AY_transform2_signVariations line 163
  15. theorem OAI.InternalCatalan.barrierCase2AY_transform2_positive_roots_le line 175