OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkActualPrincipalBlockFamilyOuterEquivBasic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.restoreOriginalDraw line 21
2. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.originalDrawAssignment_restore line 29
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.originalDrawOuter_restore line 35
4. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.originalDrawBulk_restore line 47
5. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.restoreOriginalDraw_projections line 56
6. def OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.originalDrawOuterEquiv line 67