OAI/Combinatorics/Progressions/Nilpotent/RealPolynomialBCH.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.differenceInput line 12
  2. theorem OAI.Erdos3.differenceInput_mem_denominatorGrid line 15
  3. theorem OAI.Erdos3.differenceInput_sub_mem_scaledGrid line 26
  4. theorem OAI.Erdos3.differenceCoordinate_eval line 38
  5. theorem OAI.Erdos3.differenceCoordinate_same line 59
  6. theorem OAI.Erdos3.bch_coset_eq_of_coordinate_congruence line 66
  7. def OAI.Erdos3.polynomialBCHMap line 101
  8. theorem OAI.Erdos3.polynomialBCHMap_coordinates line 107
  9. def OAI.Erdos3.polynomialBCHPeriod line 113
  10. theorem OAI.Erdos3.polynomialBCHPeriod_pos line 119
  11. theorem OAI.Erdos3.polynomialBCHMap_coset_eq line 124
  12. theorem OAI.Erdos3.polynomialBCHMap_coset_periodic_shift line 140
  13. def OAI.Erdos3.realPolynomialBCHMap line 166
  14. theorem OAI.Erdos3.realPolynomialBCHMap_coordinates line 170
  15. theorem OAI.Erdos3.contMDiff_realPolynomialBCHMap line 181
  16. theorem OAI.Erdos3.realPolynomialBCHMap_integer line 205
  17. theorem OAI.Erdos3.realification_coset_eq line 224
  18. theorem OAI.Erdos3.realPolynomialBCHMap_coset_eq line 237