OAI/Combinatorics/Progressions/Estimates/LinearDerivativeRemoval.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.linear_action_triple line 13
2. theorem OAI.Erdos3.linear_cocycle_triple line 18
3. theorem OAI.Erdos3.linear_derivative_remove line 24
4. theorem OAI.Erdos3.linear_lift_remove line 35
5. theorem OAI.Erdos3.linear_derivative_absorb line 46
6. theorem OAI.Erdos3.horizontal_lift_remove line 56
7. theorem OAI.Erdos3.horizontal_derivative_absorb line 76