OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkSupportConverseSourceUnits.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Arithmetic.HistoryBulkSupportConverse.StaticSkeleton.frequency_boundsline 15 - theorem
OAI.Ostmann.Arithmetic.HistoryBulkSupportConverse.sourceMass_coprime_paired_frequency_staticline 33 - theorem
OAI.Ostmann.Arithmetic.HistoryBulkSupportConverse.decoded_frequencyUnits_staticline 50