OAI/Combinatorics/Progressions/Fourier/CokernelCharacterWitness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.integerCokernel_character line 10
2. theorem OAI.Erdos3.integerLattice_pivot_period line 25
3. theorem OAI.Erdos3.integerCokernelExponent_le_det line 32
4. theorem OAI.Erdos3.exists_bounded_annihilating_character line 42