OAI/Combinatorics/Progressions/Estimates/QuarticFrozenMiddleExpansion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.quartic_box_eval_factors line 28
2. theorem OAI.Erdos3.quartic_box_top_layer_invariant line 36
3. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticAntisymmetricBoxNiltest_norm line 49
4. theorem OAI.Erdos3.exists_quartic_frozen_middle_expansion_of_bounds line 63