OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairBulkTransportBasic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkTransport.internalLevel_le line 12
2. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkTransport.internalLevel_ne_root line 22
3. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkTransport.root_ne_internalLevel line 27
4. def OAI.Ostmann.Arithmetic.HistoryPairBulkTransport.internalPairSample line 30
5. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkTransport.rootSample_injective line 36
6. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkTransport.samePairPattern_of_root_permutation line 47