OAI/NumberTheory/Catalan/Estimates/ManuscriptCaseOneX6SubstitutionError.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.InternalCatalan.manuscriptCase1X6SubstituteRatline 11 - theorem
OAI.InternalCatalan.manuscript_case1X6_substitute_intervalline 14 - theorem
OAI.InternalCatalan.manuscript_case1X6_substitute_cutoffline 20 - def
OAI.InternalCatalan.manuscriptCase1X6RoundedSubstituteRatline 37 - theorem
OAI.InternalCatalan.manuscript_case1X6_additional_rounding_errorline 40 - theorem
OAI.InternalCatalan.manuscript_case1X6_actual_substitution_errorline 63