OAI/Combinatorics/Progressions/Estimates/QuarticAntisymmetricModel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticCyclicMain line 13
2. theorem OAI.Erdos3.exists_quartic_reflected_model_with_mixed line 20
3. theorem OAI.Erdos3.exists_quartic_reflected_model line 130
4. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticIntegerReflection line 166
5. theorem OAI.Erdos3.exists_quartic_unwrapped_reflection_with_mixed line 175
6. theorem OAI.Erdos3.exists_quartic_unwrapped_reflection line 232
7. theorem OAI.Erdos3.exists_quartic_anchored_reflection_with_mixed line 270
8. theorem OAI.Erdos3.exists_quartic_anchored_reflection line 363
9. theorem OAI.Erdos3.exists_quartic_antisymmetric_model_with_mixed line 403
10. theorem OAI.Erdos3.exists_quartic_antisymmetric_model line 509