OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkActualTotalReplacementSquareDefs.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.Arithmetic.HistoryBulkActualTotalReplacement.plainSquareValueline 16 - def
OAI.Ostmann.Arithmetic.HistoryBulkActualTotalReplacement.plainSquareAverageline 31