OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairReferenceFlagsTransportKernels.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceFlagsTransport.leftFlag_zero_iff line 21
2. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceFlagsTransport.rightFlag_zero_iff line 26
3. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceFlagsTransport.minorFlag_zero_iff line 31
4. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceFlagsTransport.all_minors_zero_iff line 37
5. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceFlagsTransport.exists_two_nonzero_iff line 49
6. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceFlagsTransport.exists_left_nonzero_iff line 66
7. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceFlagsTransport.unitKernel_eq line 79
8. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceFlagsTransport.mixedKernel_eq line 85
9. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceFlagsTransport.symbolicKernel_eq line 91
10. theorem OAI.Ostmann.Arithmetic.HistoryPairReferenceFlagsTransport.prod_symbolicKernel_eq line 97