OAI/Combinatorics/Progressions/Polynomial/GradedPolynomialSymbolInverse.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedShiftedGradedPolynomial_coefficient line 19
2. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomialLie_coefficient line 32
3. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomialLie_graded line 40
4. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomialLie_constant line 46
5. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomialLie_linear line 59
6. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomialLie_horizontal_mem line 69
7. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomialLie_fullFast_mem line 100
8. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomialHom_coordinate line 137
9. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomialHom_bound line 147
10. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomialHom_grid line 160
11. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomialHom_correction line 184
12. def OAI.Erdos3.NilpotentLieFiltration.realSymbolOfGradedPolynomial line 212
13. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolOfGradedPolynomial_coordinate line 218
14. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomial_ofGradedPolynomial line 226
15. def OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomialHom line 243
16. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomialHom_injective line 248
17. theorem OAI.Erdos3.NilpotentLieFiltration.exists_symbol_of_gradedPolynomial line 255
18. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomialHom_native line 263
19. theorem OAI.Erdos3.NilpotentLieFiltration.symbolSlowBound_of_gradedPolynomial line 273
20. theorem OAI.Erdos3.NilpotentLieFiltration.symbolRationalGrid_of_gradedPolynomial line 280