OAI/NumberTheory/Ostmann/Arithmetic/HistorySignedResidueAverages.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistorySignedResidueAverages.unit_average_eq_four_blocks line 33
2. theorem OAI.Ostmann.Arithmetic.HistorySignedResidueAverages.mixed_average_eq_four_blocks line 53
3. theorem OAI.Ostmann.Arithmetic.HistorySignedResidueAverages.paired_unit_average_eq_four_blocks line 73
4. theorem OAI.Ostmann.Arithmetic.HistorySignedResidueAverages.paired_mixed_average_eq_four_blocks line 95