OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairReferenceSourceTransportActual.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Arithmetic.HistoryPairReferenceSourceTransport.blockReferences_slot_valuesline 33 - theorem
OAI.Ostmann.Arithmetic.HistoryPairReferenceSourceTransport.blockReferences_root_permline 43 - theorem
OAI.Ostmann.Arithmetic.HistoryPairReferenceSourceTransport.decodedSourceMean_eq_canonicalline 48