OAI/Combinatorics/Progressions/Nilpotent/StepOneGradedNiltestSplitting.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.stepOne_vertical_character line 13
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.stepOne_niltest_eval_affine line 33
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.stepOne_niltest_linear_phase_bias line 48
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_stepOne_niltest_splitting line 86
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_stepOne_graded_niltest_splitting line 147