OAI/Combinatorics/Progressions/Estimates/FormalHorizontalReabsorption.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieFiltration.formal_horizontal_logDerivative line 18
2. theorem OAI.Erdos3.NilpotentLieFiltration.formal_derivative_horizontal_balance line 36
3. theorem OAI.Erdos3.NilpotentLieFiltration.formal_extra_horizontal_equation line 68
4. theorem OAI.Erdos3.NilpotentLieFiltration.formal_lift_nonhorizontal_remainder line 91
5. theorem OAI.Erdos3.NilpotentLieFiltration.formal_logDerivative_sub_pderiv_mem_two line 135
6. theorem OAI.Erdos3.NilpotentLieFiltration.formal_reabsorption_preserves_layer_two line 146
7. theorem OAI.Erdos3.NilpotentLieFiltration.formal_degree_two_reabsorption line 186