OAI/NumberTheory/Ostmann/Preliminaries/SiftedResidues.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.SiftedWeights.forbiddenResidues line 8
2. def OAI.Ostmann.SiftedWeights.allowedResidues line 11
3. theorem OAI.Ostmann.SiftedWeights.forbiddenResidues_card line 14
4. theorem OAI.Ostmann.SiftedWeights.allowedResidues_card line 23
5. theorem OAI.Ostmann.SiftedWeights.allowedResidues_nonempty line 28
6. theorem OAI.Ostmann.SiftedWeights.allowedResidues_card_lt line 33
7. theorem OAI.Ostmann.SiftedWeights.allowedResidues_factor line 40
8. theorem OAI.Ostmann.SiftedWeights.actual_mem_allowedResidues line 48
9. theorem OAI.Ostmann.SiftedWeights.exists_shift_data line 58