OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkProducts.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryBulkProducts.bulkProduct line 10
2. def OAI.Ostmann.Arithmetic.HistoryBulkProducts.fixedProduct line 13
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkProducts.product_split line 16
4. theorem OAI.Ostmann.Arithmetic.HistoryBulkProducts.bulkProduct_append line 24
5. theorem OAI.Ostmann.Arithmetic.HistoryBulkProducts.fixedProduct_append line 27
6. theorem OAI.Ostmann.Arithmetic.HistoryBulkProducts.bulkProduct_perm line 31
7. theorem OAI.Ostmann.Arithmetic.HistoryBulkProducts.fixedProduct_perm line 36
8. theorem OAI.Ostmann.Arithmetic.HistoryBulkProducts.compensation_bulkProduct line 41
9. theorem OAI.Ostmann.Arithmetic.HistoryBulkProducts.compensation_fixedProduct line 49
10. theorem OAI.Ostmann.Arithmetic.HistoryBulkProducts.supported_product_split line 53
11. theorem OAI.Ostmann.Arithmetic.HistoryBulkProducts.supported_child_products line 62