OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkSpectatorReferenceRawLeaves.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Arithmetic.HistoryBulkSpectatorReferenceRaw.rawLeaves_eq_unitConventionline 14 - theorem
OAI.Ostmann.Arithmetic.HistoryBulkSpectatorReferenceRaw.rawLeaves_decode_slotsline 24 - theorem
OAI.Ostmann.Arithmetic.HistoryBulkSpectatorReferenceRaw.rawLeaves_decode_slots_permutedline 42