OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkResidueNormSumFrequency.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryBulkResidueNormSum.leafIndicator_norm_le line 13
2. def OAI.Ostmann.Arithmetic.HistoryBulkResidueNormSum.canonicalRTest line 22
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkResidueNormSum.canonicalRTest_norm_le line 29
4. def OAI.Ostmann.Arithmetic.HistoryBulkResidueNormSum.independentRTest line 34
5. theorem OAI.Ostmann.Arithmetic.HistoryBulkResidueNormSum.independentRTest_norm_le line 48