OAI/Combinatorics/Progressions/Polynomial/MajorWeightedDegreeTools.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.polynomialHom_preserves_weightedDegree line 16
2. def OAI.Erdos3.coordinateShearHom line 24
3. theorem OAI.Erdos3.coordinateShearHom_X line 29
4. theorem OAI.Erdos3.coordinateShearHom_rename line 38
5. theorem OAI.Erdos3.coordinateShearHom_comp_neg line 48
6. def OAI.Erdos3.coordinateShearEquiv line 63
7. theorem OAI.Erdos3.coordinateShearEquiv_apply line 69
8. theorem OAI.Erdos3.coordinateShearEquiv_symm_apply line 73
9. theorem OAI.Erdos3.coordinateShearHom_degree line 77
10. theorem OAI.Erdos3.earlierSlot_ne_self line 101
11. theorem OAI.Erdos3.exists_triangularPolynomialEquiv_prefix line 108
12. theorem OAI.Erdos3.exists_triangularPolynomialEquiv line 170
13. def OAI.Erdos3.triangularPolynomialEquiv line 182
14. theorem OAI.Erdos3.triangularPolynomialEquiv_X line 188
15. theorem OAI.Erdos3.triangularPolynomialEquiv_degree line 194
16. theorem OAI.Erdos3.triangularPolynomialEquiv_inverse_degree line 201
17. theorem OAI.Erdos3.weightedSupportLE_lt_succ line 217
18. theorem OAI.Erdos3.weightedSupportLT_map line 221
19. theorem OAI.Erdos3.weightedComparison_mul line 234
20. theorem OAI.Erdos3.weightedComparison_monomial_one line 246
21. theorem OAI.Erdos3.weightedComparison_monomial line 285
22. theorem OAI.Erdos3.weightedComparison_difference line 300
23. theorem OAI.Erdos3.totalDegree_le_of_positive_weightedSupport line 325
24. theorem OAI.Erdos3.coordinateShearHom_mass line 334
25. theorem OAI.Erdos3.coordinateShearEquiv_inverse_mass line 348
26. theorem OAI.Erdos3.exists_triangularPolynomialEquiv_prefix_mass line 365
27. theorem OAI.Erdos3.triangularPolynomialEquiv_inverse_mass line 448
28. theorem OAI.Erdos3.weightedSupportLE_totalDegree_le_of_pos line 476
29. theorem OAI.Erdos3.weightedSupportLE_of_map_injective line 481
30. theorem OAI.Erdos3.weightedSupportLE_map_iff_of_injective line 491