OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkGiantPrincipalTransportModulusCRT.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryBulkGiantPrincipalTransport.new_reference_unit_root_average line 31
2. theorem OAI.Ostmann.Arithmetic.HistoryBulkGiantPrincipalTransport.new_reference_mixed_small_average line 43