OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkFixedReferenceTransportFactorsBasic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryBulkFixedReferenceTransport.assigned_compensationProduct_eq line 16
2. theorem OAI.Ostmann.Arithmetic.HistoryBulkFixedReferenceTransport.decoded_frequencies_eq line 24
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkFixedReferenceTransport.decoded_rebuild_positiveIntegral line 36
4. theorem OAI.Ostmann.Arithmetic.HistoryBulkFixedReferenceTransport.decoded_rebuild_toHistory line 44
5. theorem OAI.Ostmann.Arithmetic.HistoryBulkFixedReferenceTransport.decoded_leafProduct_eq_residue line 53
6. theorem OAI.Ostmann.Arithmetic.HistoryBulkFixedReferenceTransport.assigned_pair_leafProduct_eq_residue line 71