OAI/Combinatorics/Progressions/Geometry/TranslationLogCoordinateScaling.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos3.PolynomialTranslationLie.translationLogMixedGroupPolynomial_eq_seriesline 13 - theorem
OAI.Erdos3.PolynomialTranslationLie.realPolynomialMass_translationLogMixedGroupPolynomialline 34 - theorem
OAI.Erdos3.PolynomialTranslationLie.translationLogMixedGroupPolynomial_coefficientGridline 48 - theorem
OAI.Erdos3.PolynomialTranslationLie.translationLogMixedGroupPolynomial_coefficientGrid_of_inputsline 59 - theorem
OAI.Erdos3.PolynomialTranslationLie.translationLogBasePolynomial_scaleline 82 - theorem
OAI.Erdos3.PolynomialTranslationLie.translationLogMixedGroupPolynomial_scaleline 90 - theorem
OAI.Erdos3.PolynomialTranslationLie.realPolynomialMass_translationLogMixedGroupPolynomial_scaleline 110