OAI/NumberTheory/Ostmann/Arithmetic/HistorySelectedJointIntegralBoundsDefs.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.Arithmetic.HistorySelectedJointIntegralBounds.bulkIntegralline 15 - def
OAI.Ostmann.Arithmetic.HistorySelectedJointIntegralBounds.nestedPrimeIntegralline 20 - def
OAI.Ostmann.Arithmetic.HistorySelectedJointIntegralBounds.nestedMixedIntegralline 25 - def
OAI.Ostmann.Arithmetic.HistorySelectedJointIntegralBounds.RectangleBoundline 30 - def
OAI.Ostmann.Arithmetic.HistorySelectedJointIntegralBounds.IntegralBoundsline 36