OAI/Combinatorics/SumProduct/Alignment/CubePolynomials01.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubePolynomials.pattern line 20
  2. def OAI.CubePolynomials.polynomials line 25
  3. lemma OAI.CubePolynomials.mem_polynomials line 28
  4. lemma OAI.CubePolynomials.polynomials_antitone line 32
  5. lemma OAI.CubePolynomials.eval_mem line 38
  6. lemma OAI.CubePolynomials.const_mem line 43
  7. lemma OAI.CubePolynomials.polynomials_eq_bot line 51
  8. def OAI.CubePolynomials.shift line 60
  9. lemma OAI.CubePolynomials.shift_mem line 67
  10. lemma OAI.CubePolynomials.derivative_mem line 77
  11. lemma OAI.CubePolynomials.mem_of_derivatives line 121
  12. lemma OAI.CubePolynomials.commutator_mem line 176
  13. lemma OAI.CubePolynomials.normalizes line 184
  14. lemma OAI.CubePolynomials.power_polynomial_mem line 202
  15. lemma OAI.NilpotentTaylor.all_derivatives_of_unit line 248
  16. lemma OAI.NilpotentTaylor.mem_of_unit_derivative line 283
  17. lemma OAI.NilpotentTaylor.binomial_mem line 289
  18. lemma OAI.NilpotentTaylor.initial_value_mem line 312
  19. lemma OAI.NilpotentTaylor.zero_of_initial line 329
  20. theorem OAI.NilpotentTaylor.determined_by_initial line 358
  21. def OAI.NilpotentTaylor.word line 370
  22. lemma OAI.NilpotentTaylor.word_mem line 374
  23. lemma OAI.NilpotentTaylor.word_congr line 382
  24. lemma OAI.NilpotentTaylor.word_update line 389
  25. lemma OAI.NilpotentTaylor.partial_taylor line 395
  26. theorem OAI.NilpotentTaylor.exists_taylor line 431