OAI/Combinatorics/Progressions/Fourier/CyclicAffineCharacterPhase.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.CircleFourier.character_sub line 11
2. theorem OAI.Erdos3.CircleFourier.exists_real_character_phase line 20
3. theorem OAI.Erdos3.CyclicBohr.exists_real_frequency_phase line 34
4. theorem OAI.Erdos3.CyclicBohr.real_frequency_phase_sub line 49
5. theorem OAI.Erdos3.CyclicBohr.exists_real_frequency_phases line 58
6. theorem OAI.Erdos3.CircleFourier.character_affine_integer_combination line 76
7. theorem OAI.Erdos3.exists_affine_cyclic_character_phase line 94