OAI/NumberTheory/Ostmann/Arithmetic/HistorySignedNumeratorsBasic.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.Arithmetic.HistorySignedNumerators.signedActualline 12 - def
OAI.Ostmann.Arithmetic.HistorySignedNumerators.actualline 20 - theorem
OAI.Ostmann.Arithmetic.HistorySignedNumerators.actual_nodeline 23 - theorem
OAI.Ostmann.Arithmetic.HistorySignedNumerators.nodeNumerator_real_signedline 37 - theorem
OAI.Ostmann.Arithmetic.HistorySignedNumerators.encoded_rows_actualline 56