OAI/NumberTheory/Ostmann/Arithmetic/HistorySmoothWeightScaleCenters.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.sourceCancellationExponent_le_nominalline 13 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.nominal_widths_leline 30