OAI/Combinatorics/Progressions/Polynomial/MajorTranslationDegreeSymbol.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.majorTranslationJointPolynomial_sub_degree_top_lower line 16
  2. theorem OAI.Erdos3.majorTranslationJointPolynomial_degree_weightedHomogeneousComponent line 28
  3. theorem OAI.Erdos3.majorTranslationJointPolynomial_degree_slot_top line 48
  4. theorem OAI.Erdos3.ofCoordinates_mem_gradedPolynomialSubmodule line 73
  5. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_of_gradedPolynomial line 101
  6. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_polynomialOrbit line 119
  7. theorem OAI.Erdos3.NilpotentLieFiltration.realCoordinatePolynomialOrbit_log_mem_graded line 129
  8. theorem OAI.Erdos3.PolynomialTranslationLie.exists_translation_coordinate_polynomialOrbit line 152
  9. theorem OAI.Erdos3.PolynomialTranslationLie.exists_majorTranslation_polynomialOrbit_of_degree line 226
  10. theorem OAI.Erdos3.PolynomialTranslationLie.exists_majorTranslation_polynomialOrbit line 245
  11. def OAI.Erdos3.PolynomialTranslationLie.translationBaseCoordinatePolynomial line 271
  12. def OAI.Erdos3.PolynomialTranslationLie.translationPolynomialCoordinatePolynomial line 276
  13. theorem OAI.Erdos3.PolynomialTranslationLie.translationBaseCoordinatePolynomial_adapted line 281
  14. theorem OAI.Erdos3.PolynomialTranslationLie.translationPolynomialCoordinatePolynomial_adapted line 290
  15. def OAI.Erdos3.PolynomialTranslationLie.translationBasePolynomialOrbit line 313
  16. def OAI.Erdos3.PolynomialTranslationLie.translationPurePolynomialOrbit line 325
  17. def OAI.Erdos3.PolynomialTranslationLie.translationCoordinatePolynomialOrbit line 338
  18. theorem OAI.Erdos3.PolynomialTranslationLie.translationBasePolynomialOrbit_log line 347
  19. theorem OAI.Erdos3.PolynomialTranslationLie.translationPurePolynomialOrbit_log line 356
  20. theorem OAI.Erdos3.PolynomialTranslationLie.translationBasePolynomialOrbit_coordinate line 366
  21. theorem OAI.Erdos3.PolynomialTranslationLie.translationPurePolynomialOrbit_coordinate line 381
  22. theorem OAI.Erdos3.PolynomialTranslationLie.translationBasePolynomialOrbit_eval_coordinates line 397
  23. theorem OAI.Erdos3.PolynomialTranslationLie.translationPurePolynomialOrbit_eval_coordinates line 413
  24. theorem OAI.Erdos3.PolynomialTranslationLie.translationBasePolynomialOrbit_realEval line 430
  25. theorem OAI.Erdos3.PolynomialTranslationLie.translationPurePolynomialOrbit_realEval line 451
  26. theorem OAI.Erdos3.PolynomialTranslationLie.translationCoordinatePolynomialOrbit_realEval line 483
  27. def OAI.Erdos3.PolynomialTranslationLie.translationPolynomialSymbolHom line 514
  28. theorem OAI.Erdos3.PolynomialTranslationLie.translationPolynomialSymbolHom_coord line 524
  29. def OAI.Erdos3.PolynomialTranslationLie.translationPolynomialSymbolLift line 532
  30. theorem OAI.Erdos3.PolynomialTranslationLie.translationPolynomialSymbolLift_log line 542
  31. theorem OAI.Erdos3.PolynomialTranslationLie.translationPolynomialSymbolHom_lift line 550
  32. theorem OAI.Erdos3.PolynomialTranslationLie.translationBasePolynomialOrbit_symbol_top line 559
  33. theorem OAI.Erdos3.PolynomialTranslationLie.translationPurePolynomialOrbit_symbol_eq_of_top line 585
  34. def OAI.Erdos3.PolynomialTranslationLie.majorTranslationPolynomialOrbit line 628
  35. theorem OAI.Erdos3.PolynomialTranslationLie.majorTranslationPolynomialOrbit_realEval line 637
  36. theorem OAI.Erdos3.PolynomialTranslationLie.majorTranslationPolynomialOrbit_top_log_graded line 652
  37. theorem OAI.Erdos3.PolynomialTranslationLie.majorTranslationPolynomialOrbit_symbol_top line 692
  38. theorem OAI.Erdos3.PolynomialTranslationLie.majorTranslationPolynomialOrbit_symbol_representative line 716
  39. theorem OAI.Erdos3.PolynomialTranslationLie.majorTranslationPolynomialOrbit_symbolLift_eq line 737
  40. theorem OAI.Erdos3.PolynomialTranslationLie.majorTranslationPolynomialOrbit_symbolLift_realEval line 761
  41. theorem OAI.Erdos3.PolynomialTranslationLie.majorTranslationPolynomialOrbit_symbol_degree_top line 791
  42. theorem OAI.Erdos3.PolynomialTranslationLie.majorTranslationPolynomialOrbit_degree_symbol_representative line 818
  43. theorem OAI.Erdos3.PolynomialTranslationLie.majorTranslationPolynomialOrbit_degree_symbolLift_eq line 841
  44. theorem OAI.Erdos3.PolynomialTranslationLie.majorTranslationPolynomialOrbit_degree_symbolLift_realEval line 863