OAI/NumberTheory/Ostmann/Arithmetic/HistoryCoefficientBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryCoefficientBounds.coefficientHistory_above line 16
2. theorem OAI.Ostmann.Arithmetic.HistoryCoefficientBounds.coefficientHistory_numerators_above line 25
3. def OAI.Ostmann.Arithmetic.HistoryCoefficientBounds.rootFreeLevel line 36
4. theorem OAI.Ostmann.Arithmetic.HistoryCoefficientBounds.coefficientHistory_rootFreeAbove line 39
5. def OAI.Ostmann.Arithmetic.HistoryCoefficientBounds.StatePolynomialFree line 49
6. theorem OAI.Ostmann.Arithmetic.HistoryCoefficientBounds.above_polynomial_free line 53
7. def OAI.Ostmann.Arithmetic.HistoryCoefficientBounds.TreePolynomialFree line 64
8. theorem OAI.Ostmann.Arithmetic.HistoryCoefficientBounds.treeAbove_polynomial_free line 71
9. theorem OAI.Ostmann.Arithmetic.HistoryCoefficientBounds.coefficientHistory_no_giant_variables line 85
10. theorem OAI.Ostmann.Arithmetic.HistoryCoefficientBounds.coefficientHistory_cost_le line 91