OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkGiantPrincipalTransportNorm.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryBulkGiantPrincipalTransport.norm_primeResidueIndicatorAt_le line 20
2. theorem OAI.Ostmann.Arithmetic.HistoryBulkGiantPrincipalTransport.norm_referenceResidueTest_le line 42
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkGiantPrincipalTransport.sum_norm_reference_primeTest_le line 58
4. theorem OAI.Ostmann.Arithmetic.HistoryBulkGiantPrincipalTransport.sum_norm_reference_mixedTest_le line 71
5. theorem OAI.Ostmann.Arithmetic.HistoryBulkGiantPrincipalTransport.sum_norm_reference_primeTest_le_modulus line 86
6. theorem OAI.Ostmann.Arithmetic.HistoryBulkGiantPrincipalTransport.sum_norm_reference_mixedTest_le_modulus line 97
7. theorem OAI.Ostmann.Arithmetic.HistoryBulkGiantPrincipalTransport.sum_norm_reference_primeTest_le_modulus_succ line 108
8. theorem OAI.Ostmann.Arithmetic.HistoryBulkGiantPrincipalTransport.sum_norm_reference_mixedTest_le_modulus_succ line 117