OAI/NumberTheory/Ostmann/Arithmetic/HistoryGiantCounterpartBoundsBasic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryGiantCounterpartBounds.role_endpoint line 16
2. theorem OAI.Ostmann.Arithmetic.HistoryGiantCounterpartBounds.H_endpoint line 24
3. theorem OAI.Ostmann.Arithmetic.HistoryGiantCounterpartBounds.U_endpoint line 37
4. lemma OAI.Ostmann.Arithmetic.HistoryGiantCounterpartBounds.root_small_positive line 43
5. lemma OAI.Ostmann.Arithmetic.HistoryGiantCounterpartBounds.roleKeys_sample_ne_zero line 47
6. theorem OAI.Ostmann.Arithmetic.HistoryGiantCounterpartBounds.H_endpoint_log_product line 54
7. theorem OAI.Ostmann.Arithmetic.HistoryGiantCounterpartBounds.U_endpoint_log_product line 76