OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkResidueRootAverageBasic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryBulkResidueRootAverage.sum_norm_average_le line 14
2. theorem OAI.Ostmann.Arithmetic.HistoryBulkResidueRootAverage.sum_norm_nested_average_le line 28
3. def OAI.Ostmann.Arithmetic.HistoryBulkResidueRootAverage.canonicalUnit line 39
4. def OAI.Ostmann.Arithmetic.HistoryBulkResidueRootAverage.canonicalMixed line 48
5. def OAI.Ostmann.Arithmetic.HistoryBulkResidueRootAverage.independentUnit line 57
6. def OAI.Ostmann.Arithmetic.HistoryBulkResidueRootAverage.independentMixed line 66