OAI/Combinatorics/Progressions/Fourier/PrimePowerTaggedCharacterRows.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.zmodAddEquiv_apply_eq_std line 12
  2. theorem OAI.Erdos3.exists_zmod_character_row line 16
  3. theorem OAI.Erdos3.primePower_character_row_primitive line 34
  4. theorem OAI.Erdos3.exists_primePower_character_primitive_row line 66
  5. theorem OAI.Erdos3.primePower_primitive_row_cast line 75
  6. theorem OAI.Erdos3.exists_primePower_character_conductor_row line 81
  7. theorem OAI.Erdos3.exists_primePower_tagged_conductor_rows line 111
  8. theorem OAI.Erdos3.exists_primePower_tagged_ambient_rows line 145