OAI/Combinatorics/Progressions/Fourier/CharacterCoordinateScale.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.latticeCharacterCoordinates line 18
  2. theorem OAI.Erdos3.integerVector_sum_single line 21
  3. theorem OAI.Erdos3.latticeCharacter_eval line 26
  4. theorem OAI.Erdos3.latticeCharacterCoordinates_injective line 43
  5. theorem OAI.Erdos3.latticeCharacterCoordinates_pow line 49
  6. theorem OAI.Erdos3.latticeCharacter_coordinate_order_dvd line 63
  7. theorem OAI.Erdos3.latticeCharacter_coordinate_order_pos line 69
  8. theorem OAI.Erdos3.latticeCharacter_order_le_product line 75
  9. theorem OAI.Erdos3.exists_coordinate_order_power_ge line 89
  10. abbrev OAI.Erdos3.TorsionLatticeCharacter line 109
  11. def OAI.Erdos3.torsionCharacterCoordinates line 112
  12. theorem OAI.Erdos3.torsionCharacterCoordinates_injective line 117
  13. instance OAI.Erdos3.torsionLatticeCharacterFintype line 126
  14. theorem OAI.Erdos3.torsionLatticeCharacter_card_le line 132
  15. theorem OAI.Erdos3.exists_coordinate_order_rpow_ge line 151