OAI/NumberTheory/Catalan/Arithmetic/FinitePlacePartialAssembly.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.determinantRat_two_adic_valuation_lower line 15
2. theorem OAI.InternalCatalan.tendsto_twoAdic_log_error line 40
3. theorem OAI.InternalCatalan.determinantRat_two_adic_eventually_lower line 70
4. def OAI.InternalCatalan.largeOddPrimeContribution line 99
5. theorem OAI.InternalCatalan.log_abs_determinantRat_place_split_lower line 104
6. theorem OAI.InternalCatalan.determinantRat_without_large_primes_eventually_lower line 113