OAI/Combinatorics/Progressions/Polynomial/PolynomialShearRealGroup.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.weightedSupportDrop_map line 13
  2. def OAI.Erdos3.polynomialShearMap line 18
  3. theorem OAI.Erdos3.polynomialShearMap_X line 24
  4. theorem OAI.Erdos3.polynomialShearMap_apply_map line 28
  5. theorem OAI.Erdos3.polynomialShearMap_add line 38
  6. theorem OAI.Erdos3.polynomialShearMap_smul line 48
  7. theorem OAI.Erdos3.polynomialShearMap_lie line 57
  8. theorem OAI.Erdos3.polynomialShearMap_monomial line 69
  9. theorem OAI.Erdos3.polynomialShearMap_basis line 78
  10. theorem OAI.Erdos3.polynomialShearMap_zero line 97
  11. theorem OAI.Erdos3.polynomialShearMap_sum line 105
  12. theorem OAI.Erdos3.polynomialShearMap_comp line 114
  13. def OAI.Erdos3.polynomialShearRationalRealMap line 135
  14. def OAI.Erdos3.polynomialShearRealificationMap line 143
  15. theorem OAI.Erdos3.polynomialShearRealificationMap_tmul line 148
  16. def OAI.Erdos3.polynomialShearRealificationHom line 152
  17. theorem OAI.Erdos3.polynomialShearRealificationHom_basis line 170
  18. def OAI.Erdos3.polynomialShearRealificationLinearEquiv line 176
  19. theorem OAI.Erdos3.polynomialShearRealificationMap_eq line 181
  20. def OAI.Erdos3.polynomialShearRealificationEquiv line 195
  21. theorem OAI.Erdos3.polynomialShearRealificationEquiv_tmul line 202
  22. theorem OAI.Erdos3.weightedSupportLE_map line 218
  23. theorem OAI.Erdos3.polynomialShearMap_pow_apply line 223
  24. theorem OAI.Erdos3.polynomialShearExp_map line 235
  25. def OAI.Erdos3.polynomialShearRealificationRatHom line 259
  26. def OAI.Erdos3.polynomialShearRealGroupEquiv line 266
  27. def OAI.Erdos3.polynomialShearRealAutEquiv line 276
  28. theorem OAI.Erdos3.polynomialShearRealAutEquiv_apply line 280
  29. theorem OAI.Erdos3.polynomialShearRealAutEquiv_rational line 285