OAI/NumberTheory/Ostmann/Arithmetic/HistorySelectedJointIntegralBoundsSource.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Arithmetic.HistorySelectedJointIntegralBounds.source_integralBounds_eventuallyline 18 - theorem
OAI.Ostmann.Arithmetic.HistorySelectedJointIntegralBounds.corrected_integrals_leline 31 - theorem
OAI.Ostmann.Arithmetic.HistorySelectedJointIntegralBounds.plain_integrals_leline 66