OAI/Combinatorics/Progressions/Polynomial/TranslationLogCoordinatePolynomials.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.PolynomialTranslationLie.shear_sum_apply line 16
  2. def OAI.Erdos3.PolynomialTranslationLie.translationLogPolynomialShear line 29
  3. def OAI.Erdos3.PolynomialTranslationLie.translationLogBasePolynomial line 35
  4. def OAI.Erdos3.PolynomialTranslationLie.translationLogPhasePolynomial line 39
  5. theorem OAI.Erdos3.PolynomialTranslationLie.translationLogPolynomialShear_base line 45
  6. theorem OAI.Erdos3.PolynomialTranslationLie.translationLogPolynomialShear_phase line 63
  7. theorem OAI.Erdos3.PolynomialTranslationLie.translationLogPolynomialShear_specialize line 80
  8. def OAI.Erdos3.PolynomialTranslationLie.translationLogGroupPolynomial line 91
  9. theorem OAI.Erdos3.PolynomialTranslationLie.translationLogGroupPolynomial_base line 98
  10. theorem OAI.Erdos3.PolynomialTranslationLie.translationLogGroupPolynomial_specialize line 103
  11. def OAI.Erdos3.PolynomialTranslationLie.translationLogMixedGroupPolynomial line 115
  12. theorem OAI.Erdos3.PolynomialTranslationLie.translationLogMixedGroupPolynomial_specialize line 120
  13. theorem OAI.Erdos3.PolynomialTranslationLie.translationLogMixedGroupPolynomial_eval line 131