OAI/Combinatorics/Progressions/Polynomial/WeightedPolynomialRestriction.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.substitute_update_add line 14
  2. theorem OAI.Erdos3.VectorPolynomial.coefficients_substitute_update_sub_mem line 31
  3. def OAI.Erdos3.MultidegreeLieFiltration.Adapted line 61
  4. def OAI.Erdos3.MultidegreeLieFiltration.adaptedSubmodule line 64
  5. theorem OAI.Erdos3.MultidegreeLieFiltration.monomial_mem_adaptedSubmodule line 74
  6. theorem OAI.Erdos3.MultidegreeLieFiltration.lie_mem_adaptedSubmodule line 83
  7. def OAI.Erdos3.MultidegreeLieFiltration.adaptedLieSubalgebra line 100
  8. theorem OAI.Erdos3.MultidegreeLieFiltration.adapted_ordinary line 103
  9. def OAI.Erdos3.MultidegreeLieFiltration.polynomialSubgroup line 110
  10. abbrev OAI.Erdos3.MultidegreeLieFiltration.PolynomialOrbit line 115
  11. def OAI.Erdos3.MultidegreeLieFiltration.PolynomialOrbit.log line 117
  12. theorem OAI.Erdos3.MultidegreeLieFiltration.PolynomialOrbit.adapted line 119
  13. def OAI.Erdos3.MultidegreeLieFiltration.polynomialOrbitEval line 121
  14. theorem OAI.Erdos3.MultidegreeLieFiltration.polynomialOrbitEval_coord line 124
  15. def OAI.Erdos3.MultidegreeLieFiltration.toOrdinaryOrbit line 127
  16. theorem OAI.Erdos3.MultidegreeLieFiltration.toOrdinaryOrbit_eval line 132
  17. theorem OAI.Erdos3.multidegreeWeight_finsupp line 145
  18. def OAI.Erdos3.MultidegreeLieFiltration.WeightedAdapted line 156
  19. def OAI.Erdos3.MultidegreeLieFiltration.weightedAdaptedSubmodule line 159
  20. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedAdapted_monomial line 172
  21. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedAdapted_lie line 182
  22. def OAI.Erdos3.MultidegreeLieFiltration.weightedAdaptedLieSubalgebra line 201
  23. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedAdapted_bch line 205
  24. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedAdapted_constant line 210
  25. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedAdapted_substitute line 215
  26. def OAI.Erdos3.omittedCoordinateWeight line 245
  27. theorem OAI.Erdos3.omittedCoordinateWeight_le_one line 247
  28. theorem OAI.Erdos3.omittedCoordinateWeight_total line 251
  29. def OAI.Erdos3.splitCoordinatePolynomial line 258
  30. theorem OAI.Erdos3.splitCoordinatePolynomial_support line 262
  31. theorem OAI.Erdos3.splitCoordinatePolynomial_zero_support line 272
  32. theorem OAI.Erdos3.splitCoordinatePolynomial_eval line 283
  33. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedAdapted_coefficients_mem line 302
  34. def OAI.Erdos3.MultidegreeLieFiltration.restrictWeightedPolynomial line 319
  35. theorem OAI.Erdos3.MultidegreeLieFiltration.restrictWeightedPolynomial_adapted line 325
  36. theorem OAI.Erdos3.MultidegreeLieFiltration.restrictWeightedPolynomial_eval line 341
  37. def OAI.Erdos3.MultidegreeLieFiltration.restrictWeightedOrbit line 349
  38. theorem OAI.Erdos3.MultidegreeLieFiltration.restrictWeightedOrbit_eval line 355