OAI/Combinatorics/Progressions/Polynomial/WeightedTranslationLatticePhase.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.PolynomialTranslationLie.realLattice_translation_integral line 13
2. def OAI.Erdos3.PolynomialTranslationLie.weightedTranslationPhaseQuotientMap line 33
3. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationPhaseQuotientMap_mk line 42
4. def OAI.Erdos3.PolynomialTranslationLie.weightedTranslationQuotientPhase line 47
5. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationQuotientPhase_mk line 51
6. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationQuotientPhase_norm line 56