OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkSpectatorReferenceRawBasic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryBulkSpectatorReferenceRaw.rawLeaves line 17
2. theorem OAI.Ostmann.Arithmetic.HistoryBulkSpectatorReferenceRaw.rawLeaves_left line 20
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkSpectatorReferenceRaw.rawLeaves_right line 26
4. theorem OAI.Ostmann.Arithmetic.HistoryBulkSpectatorReferenceRaw.child_bulk_coprime_static line 33
5. theorem OAI.Ostmann.Arithmetic.HistoryBulkSpectatorReferenceRaw.leafProduct_rawLeaves line 42
6. theorem OAI.Ostmann.Arithmetic.HistoryBulkSpectatorReferenceRaw.left_product_raw line 64
7. theorem OAI.Ostmann.Arithmetic.HistoryBulkSpectatorReferenceRaw.right_product_raw line 76