OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkActualPrincipalBlockFamilyOuter.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.outerNonbulk line 22
2. def OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.outerBlocks line 26
3. def OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.outerGiants line 30
4. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.outerNonbulk_originalDrawOuter line 33
5. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.outerBlocks_originalDrawOuter line 39
6. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.outerGiants_originalDrawOuter line 44
7. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.originalDrawAssignment_selectedSourceEquiv line 49
8. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.originalDrawAssignment_eq_fibreAssignment line 61