OAI/NumberTheory/OrdinaryCorrelations/HighTrace/FixedDisconnected.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.fixedDisconnected line 18
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.fixedUnlitCount line 22
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.totalUnlitCount line 25
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.disconnectedCount line 28
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.corruptedCount line 31
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.tagged_local_card_bound line 33
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listed_prime_count line 55
8. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.retained_tag_count line 66