OAI/Combinatorics/SumProduct/Alignment/BinomialDifference01.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CharacterFactorization.uniform_gamma_period_of_rational_lattice line 34
  2. theorem OAI.CharacterFactorization.uniform_smooth_factorization line 55
  3. def OAI.BinomialDifference.step line 96
  4. def OAI.BinomialDifference.coefficient line 98
  5. lemma OAI.BinomialDifference.step_apply line 100
  6. lemma OAI.BinomialDifference.coefficient_apply line 101
  7. lemma OAI.BinomialDifference.coefficient_zero line 102
  8. lemma OAI.BinomialDifference.coefficient_succ line 103
  9. lemma OAI.BinomialDifference.iterate_map line 106
  10. lemma OAI.BinomialDifference.coefficient_map line 115
  11. lemma OAI.BinomialDifference.step_degree_lt line 121
  12. lemma OAI.BinomialDifference.iterate_eq_zero line 124
  13. lemma OAI.BinomialDifference.coefficient_eq_zero line 139
  14. def OAI.BinomialDifference.matrix line 142
  15. lemma OAI.BinomialDifference.matrix_low line 144
  16. lemma OAI.BinomialDifference.coefficient_X_pow line 148
  17. lemma OAI.BinomialDifference.coefficient_expansion line 152
  18. lemma OAI.BinomialDifference.step_choose line 161
  19. lemma OAI.BinomialDifference.step_choose_zero line 168
  20. lemma OAI.BinomialDifference.coefficient_choose line 171
  21. lemma OAI.BinomialDifference.coefficient_word line 183
  22. def OAI.BinomialDifference.conversionBound line 204
  23. lemma OAI.BinomialDifference.conversionBound_pos line 207
  24. lemma OAI.BinomialDifference.row_bound line 213
  25. lemma OAI.BinomialDifference.coefficient_bound line 222
  26. lemma OAI.BinomialDifference.word_coefficient_bound line 262