OAI/Combinatorics/Progressions/Polynomial/ProductPolynomialMaps.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieFiltration.piRealOrbit_projection_log line 14
2. def OAI.Erdos3.RationalFilteredNilmanifold.productRestrictionIndex line 39
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestriction_coordinates line 45
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestriction_layers line 52
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestriction_lattice line 59
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestriction_realLattice line 69
7. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRestriction_piRealOrbit_log line 75