OAI/Combinatorics/Progressions/Nilpotent/NativeSquareNiltest.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieFiltration.exists_square_quotient_niltest_with_orbit line 25
2. theorem OAI.Erdos3.NilpotentLieFiltration.exists_square_quotient_niltest line 86
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_square_niltest_with_budget line 145
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_square_niltest_with_budget_and_orbit line 265
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_square_niltest_with_budget line 301
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_specified_square_niltest line 339
7. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_prescribed_two_shift_square_niltest line 457
8. def OAI.Erdos3.NativeSquareNiltestSpec line 553
9. theorem OAI.Erdos3.exists_native_square_niltest line 609