OAI/Combinatorics/Progressions/Lattices/WeightedTranslationCentralLattice.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.PolynomialTranslationLie.centralRationalElement line 13
2. def OAI.Erdos3.PolynomialTranslationLie.centralRationalLine line 18
3. theorem OAI.Erdos3.PolynomialTranslationLie.bchTranslationHom_centralRationalLine line 22
4. theorem OAI.Erdos3.PolynomialTranslationLie.centralRationalLine_mem_lattice line 30
5. theorem OAI.Erdos3.PolynomialTranslationLie.bchRealTranslationHom_realification_centralRationalLine line 39
6. theorem OAI.Erdos3.PolynomialTranslationLie.realification_centralRationalLine_mem_realLattice line 52
7. theorem OAI.Erdos3.PolynomialTranslationLie.centralRealLine_rat line 59
8. theorem OAI.Erdos3.PolynomialTranslationLie.centralRealLine_int_mem_realLattice line 66
9. theorem OAI.Erdos3.PolynomialTranslationLie.centralRealLine_mem_realLattice_iff line 75
10. theorem OAI.Erdos3.PolynomialTranslationLie.centralRealLine_int_smul line 99
11. theorem OAI.Erdos3.PolynomialTranslationLie.centralRealLine_add_int_smul line 107
12. theorem OAI.Erdos3.PolynomialTranslationLie.centralRealLine_smul_eq_iff line 116