OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkResidueNormSumActual.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryBulkResidueNormSum.actual_bulk_modulus_ne_zero line 13
2. theorem OAI.Ostmann.Arithmetic.HistoryBulkResidueNormSum.sum_norm_canonicalUnitTest_actual_modulus line 19
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkResidueNormSum.sum_norm_canonicalMixedTest_actual_modulus line 33
4. theorem OAI.Ostmann.Arithmetic.HistoryBulkResidueNormSum.sum_norm_independentUnitTest_actual_modulus line 47
5. theorem OAI.Ostmann.Arithmetic.HistoryBulkResidueNormSum.sum_norm_independentMixedTest_actual_modulus line 61