OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairFlags.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Arithmetic.HistoryPairFlags.Index line 13
2. def OAI.Ostmann.Arithmetic.HistoryPairFlags.polynomial line 16
3. theorem OAI.Ostmann.Arithmetic.HistoryPairFlags.index_card line 22
4. theorem OAI.Ostmann.Arithmetic.HistoryPairFlags.fiber_level line 27
5. theorem OAI.Ostmann.Arithmetic.HistoryPairFlags.polynomial_scope line 31
6. theorem OAI.Ostmann.Arithmetic.HistoryPairFlags.polynomial_degree line 41
7. def OAI.Ostmann.Arithmetic.HistoryPairFlags.envelope line 51
8. theorem OAI.Ostmann.Arithmetic.HistoryPairFlags.polynomial_eval_bound line 54
9. theorem OAI.Ostmann.Arithmetic.HistoryPairFlags.polynomial_integer_log_bound line 68
10. theorem OAI.Ostmann.Arithmetic.HistoryPairFlags.noAccidentalFlags_iff line 80