OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkReferenceFrequencyFamilyDefs.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.SupportedReference line 9
2. abbrev OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.ReferenceFamily line 27
3. def OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.Present line 32
4. instance OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.presentFintype line 35
5. def OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.selected line 41
6. def OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.leftHistory line 44
7. def OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.rightHistory line 47
8. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.leftHistory_supported line 50
9. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.rightHistory_supported line 53
10. theorem OAI.Ostmann.Arithmetic.HistoryBulkReferenceFrequencyFamily.supported_assignment_injective line 56