OAI/Combinatorics/Progressions/Polynomial/TranslationPolynomialSymbolLiftHom.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.lieHomSubalgebra line 12
  2. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_homogeneous_lie line 24
  3. def OAI.Erdos3.NilpotentLieFiltration.realHomogeneousAssociatedGradedMapQ line 39
  4. def OAI.Erdos3.NilpotentLieFiltration.realHomogeneousSymbolRepresentativeLie line 46
  5. theorem OAI.Erdos3.NilpotentLieFiltration.realHomogeneousSymbolRepresentativeLie_apply line 52
  6. def OAI.Erdos3.NilpotentLieFiltration.realHomogeneousAdaptedSymbolRepresentativeLie line 57
  7. def OAI.Erdos3.NilpotentLieFiltration.realHomogeneousPolynomialSymbolLiftHom line 65
  8. theorem OAI.Erdos3.NilpotentLieFiltration.realHomogeneousPolynomialSymbolLiftHom_apply line 69
  9. def OAI.Erdos3.PolynomialTranslationLie.translationPolynomialSymbolLiftHom line 85
  10. theorem OAI.Erdos3.PolynomialTranslationLie.translationPolynomialSymbolLiftHom_apply line 95
  11. theorem OAI.Erdos3.PolynomialTranslationLie.translationPolynomialSymbolLift_one line 103
  12. theorem OAI.Erdos3.PolynomialTranslationLie.translationPolynomialSymbolLift_mul line 109
  13. theorem OAI.Erdos3.PolynomialTranslationLie.translationPolynomialSymbolLift_factorization line 116