OAI/Combinatorics/Progressions/Lattices/NativePairAffineCellStepDrop.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.RationalFilteredNilmanifold.pairOrbit_substitute_log line 19
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.pairOrbitSymbol_scalarAffine_substitute line 33
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.pairOrbitSymbol_scalarAffinePullback line 63
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.pairOrbitSymbol_scalarAffinePullback_inverse_stride line 75
5. theorem OAI.Erdos3.NilpotentLieFiltration.ControlledSymbolFactorizationAtFast.dilate_ratio line 106
6. theorem OAI.Erdos3.NilpotentLieFiltration.ControlledSymbolFactorization.dilate_ratio line 141
7. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffineCell_controlled_factorization_to_original line 169
8. theorem OAI.Erdos3.exists_native_pair_affine_cell_step_drop line 205