OAI/Combinatorics/Progressions/Geometry/GlobalChartNativeFactorization.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.weightedTop_aeval_monomial line 16
  2. theorem OAI.Erdos3.coeff_aeval_monomial_eq_top line 33
  3. theorem OAI.Erdos3.NilpotentLieFiltration.adapted_realChartSubstitute_homogeneous line 57
  4. def OAI.Erdos3.NilpotentLieFiltration.homogeneousAdaptedRealChartLie line 79
  5. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousAdaptedRealChartLie_coe line 95
  6. def OAI.Erdos3.NilpotentLieFiltration.homogeneousAdaptedRealChartHom line 102
  7. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousAdaptedRealChartHom_coord line 109
  8. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolHom_homogeneousAdaptedRealChart line 117
  9. theorem OAI.Erdos3.NilpotentLieFiltration.adapted_realChartSubstitute_weightedSupport line 142
  10. def OAI.Erdos3.NilpotentLieFiltration.weightedAdaptedRealChartLie line 164
  11. theorem OAI.Erdos3.NilpotentLieFiltration.weightedAdaptedRealChartLie_coe line 180
  12. def OAI.Erdos3.NilpotentLieFiltration.weightedAdaptedRealChartHom line 187
  13. theorem OAI.Erdos3.NilpotentLieFiltration.weightedAdaptedRealChartHom_coord line 194
  14. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolOfPolynomial_chart_eq_top line 217
  15. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolOfPolynomial_inhomogeneousChart line 251
  16. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolHom_weightedAdaptedRealChart line 265
  17. theorem OAI.Erdos3.weightedRealChart_comp_support line 292
  18. theorem OAI.Erdos3.NilpotentLieFiltration.weightedAdaptedRealChartLie_comp line 309
  19. theorem OAI.Erdos3.NilpotentLieFiltration.weightedAdaptedRealChartHom_comp line 322
  20. theorem OAI.Erdos3.NilpotentLieFiltration.weightedAdaptedRealChartHom_comp_eq line 336
  21. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolHomogeneousPullback_mem_pointwise line 363
  22. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolFactorization_weightedChart line 377
  23. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolFactorization_integerChart line 397
  24. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialRealValueHom_weightedChart line 434
  25. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialRealValueHom_weightedChart_eq_of_fixed line 444
  26. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolHomogeneousPullback_mem_of_range line 456
  27. theorem OAI.Erdos3.NilpotentLieFiltration.exists_global_native_factors_of_symbol line 473