OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkActualUniversalPrincipalAlignmentPointKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryBulkActualUniversalPrincipal.alignmentSymbolicFamily line 40
2. def OAI.Ostmann.Arithmetic.HistoryBulkActualUniversalPrincipal.alignmentMatchedOuter line 44
3. def OAI.Ostmann.Arithmetic.HistoryBulkActualUniversalPrincipal.alignmentReferenceKernelProduct line 49
4. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualUniversalPrincipal.symbolic_kernel_product_eq_reference line 67
5. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualUniversalPrincipal.matched_kernel_product_eq_reference line 76
6. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualUniversalPrincipal.symbolic_present_kernel_product_eq_matched line 86