OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/ShiftedDual.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.OrdinaryShortDual.shiftedDualline 23 - lemma
OAI.OrdinaryShortDual.shiftedDual_boundline 26 - theorem
OAI.OrdinaryShortDual.dual_fubiniline 33