OAI/Combinatorics/Progressions/Polynomial/PolynomialTranslationActionCompatibility.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerCoefficientPolynomials line 13
  2. theorem OAI.Erdos3.mem_integerCoefficientPolynomials line 16
  3. theorem OAI.Erdos3.mem_integerCoefficientPolynomials_iff line 20
  4. theorem OAI.Erdos3.integerCoefficientPolynomials_X line 32
  5. theorem OAI.Erdos3.integerCoefficientPolynomials_C line 36
  6. theorem OAI.Erdos3.integerCoefficientPolynomials_rat_smul line 40
  7. theorem OAI.Erdos3.integerPolynomialHom_preserves line 50
  8. theorem OAI.Erdos3.integerPolynomialDerivation_preserves line 69
  9. theorem OAI.Erdos3.integerPolynomialDerivation_pow line 88
  10. def OAI.Erdos3.PolynomialTranslationGroupOver.actionHom line 107
  11. theorem OAI.Erdos3.PolynomialTranslationGroupOver.actionHom_X_inl line 112
  12. theorem OAI.Erdos3.PolynomialTranslationGroupOver.actionHom_X_inr line 115
  13. theorem OAI.Erdos3.PolynomialTranslationGroupOver.actionHom_C line 119
  14. theorem OAI.Erdos3.PolynomialTranslationGroupOver.actionHom_rename line 122
  15. theorem OAI.Erdos3.PolynomialTranslationGroupOver.actionHom_one line 130
  16. theorem OAI.Erdos3.PolynomialTranslationGroupOver.actionHom_mul line 137
  17. def OAI.Erdos3.PolynomialTranslationGroupOver.action line 152
  18. def OAI.Erdos3.PolynomialTranslationGroupOver.actionMonoidHom line 163
  19. theorem OAI.Erdos3.PolynomialTranslationGroupOver.actionMonoidHom_injective line 169
  20. theorem OAI.Erdos3.polynomialTranslate_map_ring line 196
  21. def OAI.Erdos3.PolynomialTranslationGroupOver.map line 207
  22. theorem OAI.Erdos3.PolynomialTranslationGroupOver.map_base line 219
  23. theorem OAI.Erdos3.PolynomialTranslationGroupOver.map_polynomial line 222
  24. def OAI.Erdos3.PolynomialTranslationGroupOver.actionElement line 235
  25. theorem OAI.Erdos3.PolynomialTranslationGroupOver.actionElement_X_inl line 238
  26. theorem OAI.Erdos3.PolynomialTranslationGroupOver.actionElement_X_inr line 242
  27. theorem OAI.Erdos3.PolynomialTranslationGroupOver.action_eq_of_shape line 249
  28. theorem OAI.Erdos3.PolynomialTranslationGroupOver.existsUnique_action_of_shape line 262
  29. theorem OAI.Erdos3.eval_polynomialTranslate_ring line 280
  30. theorem OAI.Erdos3.PolynomialTranslationGroupOver.action_inverse_X_inl_eval line 289
  31. theorem OAI.Erdos3.PolynomialTranslationGroupOver.action_inverse_X_inr_eval line 299
  32. theorem OAI.Erdos3.PolynomialTranslationGroupOver.phase_argument_eq_inverse_point line 311
  33. theorem OAI.Erdos3.integerCoefficientPolynomials_C_iff line 331
  34. theorem OAI.Erdos3.integerCoefficientPolynomials_rename line 341
  35. theorem OAI.Erdos3.integerCoefficientPolynomials_rename_iff line 347
  36. theorem OAI.Erdos3.integerCoefficientPolynomials_translate line 359
  37. theorem OAI.Erdos3.integerCoefficientPolynomials_translate_iff line 370
  38. theorem OAI.Erdos3.PolynomialTranslationGroupOver.map_actionHom line 393
  39. def OAI.Erdos3.PolynomialTranslationGroupOver.rationalEquiv line 410
  40. theorem OAI.Erdos3.PolynomialTranslationGroupOver.rationalEquiv_action line 417