OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkSourceDisintegrationSelectedDefs.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.SelectedTemplate line 12
2. theorem OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.selected_bulk_source line 15
3. abbrev OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.SelectedNonbulkSample line 22
4. abbrev OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.SelectedBulkSample line 25
5. def OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.selectedNonbulkPrior line 28
6. def OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.selectedBulkPrior line 31
7. def OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.selectedSourceEquiv line 35
8. theorem OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.selectedSourceEquiv_nonbulk line 41
9. theorem OAI.Ostmann.Arithmetic.HistoryBulkSourceDisintegration.selectedSourceEquiv_bulk_val line 46