OAI/Combinatorics/Progressions/Polynomial/PolynomialShearWeightedOrbitCoordinates.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.polynomialShearReal_adapted_iff_coordinate_support line 16
  2. def OAI.Erdos3.polynomialShearOrbitParameterCoordinates line 48
  3. theorem OAI.Erdos3.polynomialShearOrbitParameterCoordinates_degree line 54
  4. theorem OAI.Erdos3.polynomialShearOrbitParameterCoordinates_eval line 61
  5. theorem OAI.Erdos3.polynomialShearOrbitParameterCoordinates_reconstruct line 71
  6. theorem OAI.Erdos3.patchParameterSpecialization_rename_parameter line 91
  7. theorem OAI.Erdos3.patchParameterSpecialization_rename_slot line 101
  8. theorem OAI.Erdos3.polynomialSymbolicShearTerm_specialization line 113
  9. theorem OAI.Erdos3.polynomialSymbolicShearSlot_specialization line 121
  10. theorem OAI.Erdos3.polynomialShearOrbitSymbolicDerivation_X_slot_specialization line 142
  11. theorem OAI.Erdos3.polynomialShearOrbitSymbolicDerivation_specialization line 151
  12. theorem OAI.Erdos3.polynomialShearOrbitSymbolicExp_specialization line 165
  13. theorem OAI.Erdos3.weightedPolynomialShearReal_adapted_iff_coordinate_support line 188
  14. def OAI.Erdos3.weightedPolynomialShearOrbitParameterCoordinates line 220
  15. theorem OAI.Erdos3.weightedPolynomialShearOrbitParameterCoordinates_degree line 226
  16. theorem OAI.Erdos3.weightedPolynomialShearOrbitParameterCoordinates_eval line 233
  17. theorem OAI.Erdos3.weightedPolynomialShearOrbitParameterCoordinates_reconstruct line 243
  18. theorem OAI.Erdos3.weightedPolynomialShearOrbitSymbolicDerivation_X_slot_specialization line 267
  19. theorem OAI.Erdos3.weightedPolynomialShearOrbitSymbolicDerivation_specialization line 276
  20. theorem OAI.Erdos3.weightedPolynomialShearOrbitSymbolicExp_specialization line 290