OAI/Combinatorics/Progressions/Polynomial/PolynomialShearFactorialIntegrality.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.WeightedLoweringAut.difference_pow_degree line 16
  2. theorem OAI.Erdos3.WeightedLoweringAut.difference_pow_lower line 25
  3. def OAI.Erdos3.polynomialShearLogOn line 33
  4. theorem OAI.Erdos3.polynomialShearLogOn_sum line 37
  5. theorem OAI.Erdos3.polynomialShearLogOn_mono line 46
  6. theorem OAI.Erdos3.polynomialShearLogOn_leibniz line 61
  7. def OAI.Erdos3.polynomialShearLogValue line 86
  8. theorem OAI.Erdos3.polynomialShearLogValue_eq_on line 91
  9. theorem OAI.Erdos3.polynomialShearLogValue_eq_sum line 97
  10. theorem OAI.Erdos3.polynomialShearLogValue_add line 104
  11. theorem OAI.Erdos3.polynomialShearLogValue_smul line 116
  12. theorem OAI.Erdos3.polynomialShearLogValue_mul line 125
  13. theorem OAI.Erdos3.polynomialShearLogValue_C line 137
  14. def OAI.Erdos3.polynomialShearLogDerivation line 142
  15. theorem OAI.Erdos3.polynomialShearLogValue_lower line 155
  16. def OAI.Erdos3.polynomialShearLog line 165
  17. theorem OAI.Erdos3.polynomialShearLog_apply line 172
  18. theorem OAI.Erdos3.polynomialShearLog_end line 187
  19. theorem OAI.Erdos3.polynomialShearExp_degreeAction line 194
  20. theorem OAI.Erdos3.polynomialShearExp_log line 201
  21. theorem OAI.Erdos3.polynomialShearLog_exp line 214
  22. def OAI.Erdos3.polynomialShearExpLogEquiv line 226
  23. theorem OAI.Erdos3.polynomialShearExpAut_injective line 233
  24. theorem OAI.Erdos3.polynomialShearExpAut_surjective line 237
  25. theorem OAI.Erdos3.polynomialShearLog_injective line 241
  26. theorem OAI.Erdos3.polynomialShearLog_surjective line 245
  27. def OAI.Erdos3.PolynomialSlots.symbolicLogSlot line 261
  28. theorem OAI.Erdos3.PolynomialSlots.symbolicLogSlot_degree line 266
  29. theorem OAI.Erdos3.PolynomialSlots.symbolicLogSlot_specialization line 273
  30. theorem OAI.Erdos3.polynomialShear_scaled_pow line 296
  31. theorem OAI.Erdos3.polynomialShear_factorial_exp_integral line 302
  32. theorem OAI.Erdos3.polynomialShear_factorial_log_integral line 316