OAI/Combinatorics/Progressions/Polynomial/ExtendedPolynomialValues.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.lie_monomial line 18
  2. def OAI.Erdos3.VectorPolynomial.evalLie line 23
  3. theorem OAI.Erdos3.VectorPolynomial.evalLie_apply line 36
  4. theorem OAI.Erdos3.VectorPolynomial.eval_lieBCH line 43
  5. theorem OAI.Erdos3.VectorPolynomial.lowerCentralSeries_eq_bot line 47
  6. def OAI.Erdos3.VectorPolynomial.outsideDownsetIdeal line 72
  7. theorem OAI.Erdos3.VectorPolynomial.mem_outsideDownsetIdeal line 97
  8. theorem OAI.Erdos3.VectorPolynomial.outsideDownsetIdeal_union line 103
  9. def OAI.Erdos3.VectorPolynomial.eval₂Lie line 124
  10. theorem OAI.Erdos3.VectorPolynomial.eval₂Lie_apply line 137
  11. theorem OAI.Erdos3.VectorPolynomial.eq_zero_of_eval_zero line 154
  12. theorem OAI.Erdos3.VectorPolynomial.eval_mem_iff_coefficients line 174
  13. def OAI.Erdos3.VectorPolynomial.coefficientSubmodule line 200
  14. theorem OAI.Erdos3.VectorPolynomial.monomial_mem_coefficientSubmodule line 210
  15. def OAI.Erdos3.VectorPolynomial.coefficientLieSubalgebra line 219
  16. theorem OAI.Erdos3.coefficient_zero_of_squarefreeKernel line 251
  17. theorem OAI.Erdos3.squarefreeKernel_lie_mem line 256
  18. def OAI.Erdos3.squarefreePolynomialIdeal line 276
  19. def OAI.Erdos3.VectorPolynomial.weightedDilation line 292
  20. theorem OAI.Erdos3.VectorPolynomial.coefficients_weightedDilation line 312
  21. theorem OAI.Erdos3.VectorPolynomial.weightedDilation_monomial line 318
  22. theorem OAI.Erdos3.VectorPolynomial.weightedDilation_one line 325
  23. theorem OAI.Erdos3.VectorPolynomial.weightedDilation_mul line 331
  24. theorem OAI.Erdos3.VectorPolynomial.weighted_monomial_dilation line 337
  25. theorem OAI.Erdos3.VectorPolynomial.eval_weightedDilation line 348
  26. theorem OAI.Erdos3.VectorPolynomial.eval₂_weightedDilation line 356
  27. theorem OAI.Erdos3.VectorPolynomial.weightedDilation_lie line 373
  28. def OAI.Erdos3.VectorPolynomial.weightedDilationLie line 389
  29. def OAI.Erdos3.VectorPolynomial.translate line 407
  30. theorem OAI.Erdos3.VectorPolynomial.translate_tmul line 410
  31. theorem OAI.Erdos3.VectorPolynomial.coefficients_translate_monomial line 413
  32. theorem OAI.Erdos3.VectorPolynomial.coefficients_translate_sub_monomial line 418
  33. theorem OAI.Erdos3.VectorPolynomial.eval_translate line 424
  34. theorem OAI.Erdos3.VectorPolynomial.map_translate line 434
  35. theorem OAI.Erdos3.VectorPolynomial.coefficients_translate line 440
  36. theorem OAI.Erdos3.VectorPolynomial.coefficients_translate_sub line 446
  37. theorem OAI.Erdos3.VectorPolynomial.eval₂_map line 469
  38. theorem OAI.Erdos3.VectorPolynomial.eq_zero_of_eval₂_zero line 482
  39. theorem OAI.Erdos3.VectorPolynomial.eval₂_mem_iff_coefficients line 500