OAI/NumberTheory/Ostmann/Arithmetic/HistorySignedResiduesModulus.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistorySignedResidues.testProduct line 9
2. theorem OAI.Ostmann.Arithmetic.HistorySignedResidues.frequencies_rebuild line 16
3. theorem OAI.Ostmann.Arithmetic.HistorySignedResidues.Covers.mono line 23
4. theorem OAI.Ostmann.Arithmetic.HistorySignedResidues.small_dvd_product line 34
5. theorem OAI.Ostmann.Arithmetic.HistorySignedResidues.testProduct_covers_rebuild line 38
6. def OAI.Ostmann.Arithmetic.HistorySignedResidues.fullTestProduct line 74
7. theorem OAI.Ostmann.Arithmetic.HistorySignedResidues.fullTestProduct_covers_rebuild line 77
8. theorem OAI.Ostmann.Arithmetic.HistorySignedResidues.outside_dvd_fullTestProduct line 81