OAI/NumberTheory/Ostmann/Arithmetic/HistoryGiantGridCellBoundsNormalization.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Arithmetic.HistoryGiantGridCellBounds.eventually_giant_normalizationline 15 - theorem
OAI.Ostmann.Arithmetic.HistoryGiantGridCellBounds.selected_giant_normalization_eventuallyline 39