OAI/NumberTheory/Catalan/Arithmetic/OddPrimeEvenBlockPartition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.evenBlock_quotient_parity line 12
2. theorem OAI.InternalCatalan.evenBlock_bounds line 20
3. theorem OAI.InternalCatalan.evenBlock_survives line 28
4. theorem OAI.InternalCatalan.evenBlock_injective line 52
5. theorem OAI.InternalCatalan.evenBlock_preimage line 68
6. theorem OAI.InternalCatalan.even_surviving_sum_eq_complete_blocks line 102