OAI/NumberTheory/Jacobsthal/Estimates/FrozenSuffixData.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos970.NumberTheoryLean.FrozenSuffixData.suffixPrimes_replacementline 13 - theorem
OAI.Erdos970.NumberTheoryLean.FrozenSuffixData.after_available_replacementline 35 - theorem
OAI.Erdos970.NumberTheoryLean.FrozenSuffixData.terminal_suffix_cutoffline 42 - theorem
OAI.Erdos970.NumberTheoryLean.FrozenSuffixData.replacement_cutoffline 52