OAI/NumberTheory/Ostmann/QuadraticCenter/AdaptiveSmallArrayDefs.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.QuadraticCenter.adaptiveSmallBaseParametersline 11 - def
OAI.Ostmann.QuadraticCenter.adaptiveOffEventParametersline 15 - def
OAI.Ostmann.QuadraticCenter.adaptiveNoSmallWitnessline 24 - def
OAI.Ostmann.QuadraticCenter.adaptiveSmallArrayline 30 - def
OAI.Ostmann.QuadraticCenter.adaptiveOffEventArrayFamilyline 37 - def
OAI.Ostmann.QuadraticCenter.adaptiveSmallArrayFamilyline 42 - theorem
OAI.Ostmann.QuadraticCenter.adaptiveSmallSupport_subsetline 47 - theorem
OAI.Ostmann.QuadraticCenter.divisorQuadraticSumP_canonical_reductionline 56