OAI/NumberTheory/Ostmann/Arithmetic/HistorySymbolicStep.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.Arithmetic.HistorySymbolicStep.productline 12 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicStep.product_evalline 16 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicStep.product_regularline 22 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicStep.product_atomCountline 28 - def
OAI.Ostmann.Arithmetic.HistorySymbolicStep.pivotline 34 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicStep.pivot_evalline 38 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicStep.supported_pivot_evalline 45 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicStep.supported_pivot_regularline 65 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicStep.pivot_atomCountline 83