OAI/Combinatorics/Progressions/Lattices/WeightedTranslationLattice.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.PolynomialTranslationLie.weightedTranslationLattice line 13
2. theorem OAI.Erdos3.PolynomialTranslationLie.mem_weightedTranslationLattice line 17
3. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationLattice_eq_integral_preimage line 23
4. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationLattice_inner_grid line 32
5. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationLattice_outer_grid line 46