OAI/Combinatorics/Progressions/Polynomial/RealAdaptedPolynomialGroup.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.mapLie line 15
  2. def OAI.Erdos3.NilpotentLieFiltration.filteredPolynomialMap line 33
  3. theorem OAI.Erdos3.NilpotentLieFiltration.filteredPolynomialMap_coe line 45
  4. theorem OAI.Erdos3.NilpotentLieFiltration.filteredPolynomialMap_mem_shiftedIdeal line 49
  5. def OAI.Erdos3.NilpotentLieFiltration.filteredPolynomialSymbolMap line 57
  6. theorem OAI.Erdos3.NilpotentLieFiltration.filteredPolynomialSymbolMap_symbol line 71
  7. def OAI.Erdos3.NilpotentLieFiltration.associatedGradedMap line 75
  8. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedMap_piece line 78
  9. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedMap_piece_eq_zero_iff line 87
  10. theorem OAI.Erdos3.NilpotentLieFiltration.filteredPolynomialMap_coefficient line 109
  11. theorem OAI.Erdos3.NilpotentLieFiltration.filteredPolynomialMap_surjective line 114
  12. theorem OAI.Erdos3.NilpotentLieFiltration.filteredPolynomialSymbolMap_surjective line 147
  13. theorem OAI.Erdos3.NilpotentLieFiltration.filteredPolynomialMap_shiftedIdeal_surjective line 171
  14. theorem OAI.Erdos3.NilpotentLieFiltration.exists_polynomial_lift_with_symbol line 208
  15. theorem OAI.Erdos3.NilpotentLieFiltration.realQuotientPolynomialOrbit_surjective line 246
  16. theorem OAI.Erdos3.NilpotentLieFiltration.realQuotientPolynomialOrbit_realEval line 271
  17. def OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialMap line 293
  18. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialMap_coefficient_tmul line 298
  19. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialMap_adapted line 307
  20. def OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialTensor line 319
  21. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialTensor_coe line 328
  22. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialTensor_coordinates line 335
  23. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialTensor_surjective line 348
  24. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedMonomialBasis_bracket_support line 390
  25. def OAI.Erdos3.NilpotentLieFiltration.scaledRealAdaptedMonomialBasis line 404
  26. theorem OAI.Erdos3.NilpotentLieFiltration.scaledRealAdaptedMonomialBasis_repr line 409
  27. theorem OAI.Erdos3.NilpotentLieFiltration.scaledRealAdaptedMonomialBasis_structure line 416
  28. theorem OAI.Erdos3.NilpotentLieFiltration.scaledRealAdaptedMonomialBasis_bound_iff line 428
  29. theorem OAI.Erdos3.NilpotentLieFiltration.realFilteredPolynomialMap_polynomial line 452
  30. abbrev OAI.Erdos3.NilpotentLieFiltration.RealAdaptedPolynomialGroup line 482
  31. def OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialGroupHom line 484
  32. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialGroupHom_log line 488
  33. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialGroupHom_surjective line 496
  34. def OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialGroupLift line 501
  35. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialGroupHom_lift line 505
  36. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialGroupHom_coordinate line 510