OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/ArithmeticTwist.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.OrdinaryArchimedeanTwist.arithmeticTwistline 22 - lemma
OAI.OrdinaryArchimedeanTwist.arithmeticTwist_applyline 25 - lemma
OAI.OrdinaryArchimedeanTwist.arithmeticTwist_mulline 28