OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkGiantPrincipalTransportActualPrincipalBasic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Ostmann.Arithmetic.HistoryBulkGiantPrincipalTransport.neZero_of_dvd_modulus line 18
2. theorem OAI.Ostmann.Arithmetic.HistoryBulkGiantPrincipalTransport.new_reference_unit_root_average_of_modulus line 34
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkGiantPrincipalTransport.new_reference_mixed_small_average_of_modulus line 51