OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoBracketYGroup0.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.barrierCase2AX_computed_coeff_35 line 11
  2. theorem OAI.InternalCatalan.barrierCase2AX_computed_coeff_36 line 15
  3. theorem OAI.InternalCatalan.barrierCase2AX_computed_coeff_small line 19
  4. theorem OAI.InternalCatalan.barrierCase2AX_coeff_computed line 62
  5. theorem OAI.InternalCatalan.barrierCase2AX_natDegree_le line 90
  6. theorem OAI.InternalCatalan.barrierCase2AX_eq_explicit line 117
  7. theorem OAI.InternalCatalan.barrierCase2AX_natDegree line 131
  8. theorem OAI.InternalCatalan.barrierCase2AX_coeff_small line 138
  9. def OAI.InternalCatalan.barrierCase2AXFiniteEval line 150
  10. def OAI.InternalCatalan.barrierCase2AYFiniteEval line 153
  11. theorem OAI.InternalCatalan.barrierCase2AX_eval_finite line 156
  12. theorem OAI.InternalCatalan.barrierCase2AY_eval_finite line 171
  13. def OAI.InternalCatalan.barrierCase2AXTransform0Coefficient line 191
  14. def OAI.InternalCatalan.barrierCase2AXTransform0Explicit line 194
  15. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_natDegree line 233
  16. def OAI.InternalCatalan.barrierCase2AXTransform1Coefficient line 237
  17. def OAI.InternalCatalan.barrierCase2AXTransform1Explicit line 240
  18. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_natDegree line 279
  19. theorem OAI.InternalCatalan.barrierCase2AX_bracket_finite_sign_00 line 285
  20. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_00 line 290
  21. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_01 line 297
  22. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_02 line 304
  23. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_03 line 311
  24. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_04 line 318
  25. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_05 line 325
  26. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_06 line 332
  27. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_07 line 339
  28. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_08 line 346
  29. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_09 line 353
  30. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_10 line 360
  31. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_11 line 367
  32. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_12 line 374
  33. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_13 line 381
  34. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_14 line 388
  35. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_15 line 395
  36. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_16 line 402
  37. theorem OAI.InternalCatalan.barrierCase2AX_bracket_sign_17 line 409
  38. theorem OAI.InternalCatalan.barrierCase2AY_bracket_sign_00 line 416
  39. theorem OAI.InternalCatalan.barrierCase2AY_bracket_sign_01 line 423
  40. theorem OAI.InternalCatalan.barrierCase2AY_bracket_sign_02 line 430