OAI/NumberTheory/OrdinaryCorrelations/HighTrace/DisconnectedWitness.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedWitness line 21
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedWitness.left_cast line 31
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedWitness.right_cast line 34
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.disconnected_witness_exists line 38
5. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair line 46
6. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.disconnected_block_pair_exists line 58
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.first_nonempty line 134
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.second_nonempty line 137
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.active_separate line 141